source: CIVL/examples/languageFeatures/struct.cvl@ ffff8f5

1.23 2.0 main test-branch
Last change on this file since ffff8f5 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: 659 bytes
Line 
1/* Commandline execution:
2 * civl verify struct.cvl
3 * */
4#include<civlc.cvh>
5
6typedef struct Interval {
7 int left;
8 int right;
9} Interval;
10
11typedef struct IntervalList {
12 Interval value;
13 Interval* next;
14} IntervalList;
15
16void main() {
17 Interval result={.left = 2, .right = 3};
18 IntervalList list1 = {.value ={.left=2, .right=3}, .next = &result};
19 IntervalList list2 = {.value = result, .next = NULL};
20
21 $assert((list1.value.left==list1.next->left && list1.value.right == list1.next->right));
22 $assert((result.left == 2 && result.right == 3));
23 result.left = 0;
24 result.right = 1;
25 $assert((result.left == 0));
26 $assert((result.right == 1));
27}
Note: See TracBrowser for help on using the repository browser.