1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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?
|
