source: CIVL/examples/analysis/abs.c@ 6df6487

1.23 2.0 main test-branch
Last change on this file since 6df6487 was cbea8be, checked in by Manchun Zheng <zmanchun@…>, 11 years ago

added new system function $pathCondition and tests; minor correction of abs call analyzer; added new keywords to emacs script; minor correction of notes for adding new options.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@2379 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 382 bytes
RevLine 
[b1b88d8]1#include <stdlib.h>
[9570bc1]2#include <civlc.cvh>
[b1b88d8]3
[e4cc4f5]4$input int k;
[9570bc1]5$input int x;
6$input int y;
7$input int z;
8$assume(x<0);
9$assume(y>0);
[e4cc4f5]10$assume(k!=0);
[b1b88d8]11void main(){
12 int a = 9;
13
[cbea8be]14 a=abs(0);
15 a=abs(x); // x<0
16 a=abs(y); // y>0
17 a=abs(z);
18 a=abs(k); // k!=0
19 a=abs(x*y*z);
[e4cc4f5]20 a=abs(x*y*k);
[cbea8be]21 a=abs(x*y);
[9570bc1]22 $assert(x*y<=0);
23
[cbea8be]24 a=abs(y%2-1);
25 a=abs(y%2-2);
[b1b88d8]26}
Note: See TracBrowser for help on using the repository browser.