Better c support

[sakehl]

I've added some better C support for several things.

• Structs
  • As discussed in Adding support for structs in C backend #1055, I've added structs (sort of like classes, but are passed by value when given to a function).
• Pointers/Arrays
• As discussed in How to treat pointers & arrays in C backend #1056. I've chosen the "No difference between pointers and arrays" for now, since that has everything working for the cases I was interested in.
• You can now declare a new array like int a[5], int a[] = {0, 1, 2, 3, 4} or int a[5] = {0, 1, 2, 3, 4}
• Casts
  • I've added support to cast between integers and floats. Although floats are still eventually encoded as rationals.
• Malloc / Free
  • malloc only works in this specific format: int *xs = (int *) malloc(5*sizeof(int)). It creates a pointer block with pointer_offset set to 0. In the example, it has a length of 5.
  • Free only works on pointer_blocks which have the pointer_offset set to 0. Furthermore, it requires write permission to the complete pointer_block, which is does not give back.
• Parallel blocks #omp parallel for
  • (TODO) How it already was working: if you give a loop an iteration contract instead of a regular contract, it is treated as par block. It would be nice if it only did that if you gave the annotation #omp parallel for? Or alternatively, if #omp parallel for is present, it requires an iteration contract.
  • Fixed a bug, where when a loop had declarations and was converted to a par block, those declarations were moved towards a higher scope, which led to internal errors.
• % in C
  • The % is now working in better correspondence with the c99 compiler. (although to be completely fair, it is compiler/architecture dependent).
  • If they ever change this in Viper, we should as well. See Inconsistent behavior of division viperproject/silver#297
  • For now at least this is working by defining % in C (cmod) as (similar as in the above mentioned issue):

function cmod(a: Int, b: Int ): Int
  requires b != 0
{
  let res == (a % b) in a > 0 || res == 0 ? res : res - abs(b)
}

cmod(36, 7) == 1
cmod(-36, 7) == -1
cmod(36, -7) == -1
cmod(-36, -7) == -1

• Fixed a bug where inline and pure annotations were not actually processed
• I've defined some header files
  • Mostly all (un)signed integers are mapped to int
  • Mostly all float types are mapped to float (but actually rational)

I did not make any test cases yet, which I could still make.

In some cases, I really had no clue how to get the correct blame for a node. So I made PanicBlame("TODO") in those cases, any advice on those would be great.

[pieter-bos]

Hey, nice work! I am ok with the general structure of the changes and I've tried to provide some useful feedback. If there's particular areas you want me to have a more detailed look at feel free to let me know.

[sakehl]

I am finished with everything now. And I tried to comment on some stuff you wrote or fix what you were saying.

I've tried to include tests for all the functionality I wrote. The bigger things in the files. The potential errors/verification failures as smaller tests in CSpec.scala.

How would you want me to proceed @pieter-bos ?

[pieter-bos]

Very nice work! Let's get it merged (I'm just running the test suite now, since GitHub doesn't do that for forks)

[sakehl]

Awesome, glad that it's merged!