Context Navigation

mem_convertion3.cvl@ cc8e265

1.23 2.0 acw/focus-triggers main test-branch

Last change on this file since cc8e265 was da65ee2, checked in by Ziqing Luo <ziqing@…>, 7 years ago

re-implemented loop invariants using $mem for transformation and valueSetRef for reasoning

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

File size: 228 bytes

Rev	Line
[da65ee2]	1	#include<mem.cvh>
	2	#include<pointer.cvh>
	3
	4	int main() {
	5	$mem m;
	6	int * a;
	7	int b;
	8	int c[10];
	9
	10	a = &b;
	11	// referecne to variable with undefined value
	12	m = a;
	13	a = &c[0];
	14	m = a + (0 .. 9);
	15	$assert($equals(&m, &m));
	16	}

Note: See TracBrowser for help on using the repository browser.