source: CIVL/examples/languageFeatures/int2char.cvl@ b2a2faa

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

updated examples since $assert/$assume has been changed to functions; fixed the model builder for the new side-effect remover.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@2085 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 488 bytes
RevLine 
[9803bc1]1#include <civlc.cvh>
[c6291e9]2#include <stdio.h>
3
4$input int num;
[3ff27cf]5$assume(num > 0 && num < 255);
[c6291e9]6void main(){
7 char c[3];
8 char * pc;
9 int b = 98; // 'b'
10
11 pc = (char*)$malloc($root, sizeof(char) * 3);
12 c[0] = num;
13 c[1] = 'a';
14 c[2] = b - 1;
15
16 pc[0] = num;
17 pc[1] = b - 1;
18 pc[2] = 97;
19 //test symbolic int to char
[3ff27cf]20 $assert((c[0] == pc[0]));
[c6291e9]21 //test if (char)(b-1) == 'a'
[3ff27cf]22 $assert((c[1] == pc[1]));
[c6291e9]23 //test if (char)(98 - 1) == (char)97
[3ff27cf]24 $assert((c[2] == pc[2]));
[c6291e9]25 $free(pc);
26}
Note: See TracBrowser for help on using the repository browser.