source:
CIVL/examples/languageFeatures/int2char.cvl@
44512b7
| Last change on this file since 44512b7 was d980649, checked in by , 10 years ago | |
|---|---|
|
|
| File size: 482 bytes | |
| Rev | Line | |
|---|---|---|
| [9803bc1] | 1 | #include <civlc.cvh> |
| [c6291e9] | 2 | #include <stdio.h> |
| 3 | ||
| 4 | $input int num; | |
| [3ff27cf] | 5 | $assume(num > 0 && num < 255); |
| [c6291e9] | 6 | void 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 | |
| [d980649] | 20 | $assert(c[0] == pc[0]); |
| [c6291e9] | 21 | //test if (char)(b-1) == 'a' |
| [d980649] | 22 | $assert(c[1] == pc[1]); |
| [c6291e9] | 23 | //test if (char)(98 - 1) == (char)97 |
| [d980649] | 24 | $assert(c[2] == pc[2]); |
| [c6291e9] | 25 | $free(pc); |
| 26 | } |
Note:
See TracBrowser
for help on using the repository browser.
