why3/plugins/microc

A plugin to verify programs written in a (microscopic) fragment of C.
Designed for teaching purposes.

See tests/microc/*.c for examples.

Differences/limitations wrt C:
- types are limited to integers and arrays of integers
- integers of type 'int' only, and assumed to be of arbitrary precision
- arrays can be stack allocated or passed as arguments, but cannot be returned
- scanf is limited to scanf("%d", &x)
- a call to printf is ignored (but arguments are evaluated first)
- rand() returns a nonnegative integer, but with no upper limit (no RAND_MAX);
  not an issue when used in expressions such as a+rand()%(b-a+1)
- assignments expressions do not have a value (so one cannot write x=y=0)

Todo:
- lemma function?