mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
059c2b5473
multi-lines spec comments /*@ ... */ axioms, with syntax //@ assume ...; assignments operators ++ -- += etc. for array elements
18 lines
723 B
Plaintext
18 lines
723 B
Plaintext
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?
|