source: CIVL/mods/dev.civl.com/examples/analysis/abs.c@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

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