Cascade User Manual - Revision history

Baoluo-meng at 16:34, 1 March 2017

2017-03-01T16:34:36Z

2012-12-20T01:17:30Z

‎Command line

2012-12-19T20:49:57Z

‎Build and Install Cascade

2012-12-18T03:28:15Z

‎Options

2012-12-18T03:26:55Z

‎Reachability

2012-12-17T23:36:31Z

‎Reachability

2012-12-17T23:35:19Z

‎Reachability

2012-12-17T22:51:21Z

‎Logic Operators and Predicates

2012-12-17T22:50:45Z

‎Logic Operators and Predicates

2012-12-17T22:50:02Z

‎Logic Operators and Predicates

@@ Line 16: / Line 16: @@
 == Build and Install CVC4 ==
-* Please check the instructions on visit the [http://cvc4.cs.nyu.edu/wiki/User_Manual#Getting_CVC4 Getting CVC4]. Note that, the directory I used to install CVC4 is "/Users/Wei/Workspace/target/cvc4".
+* Please check the instructions on visit the [http://cvc4.cs.stanford.edu/web/#Getting_CVC4 Getting CVC4]. Note that, the directory I used to install CVC4 is "/Users/Wei/Workspace/target/cvc4".
 * For Linux, add library to the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH for Mac) in ~/.bashrc (or profile).
       export LD_LIBRARY_PATH=/Users/Wei/Workspace/target/cvc4/lib:$LD_LIBRARY_PATH

@@ Line 54: / Line 54: @@
 * Make sure LD_LIBRARY_PATH (DYLD_LIBRARY_PATH for Mac) includes the directory the cvc4jni library and the cvc4 library are installed
      export LD_LIBRARY_PATH=/Users/Wei/Workspace/target/cvc4/lib:$LD_LIBRARY_PATH
 * The cascade tool can be run using "c/target/cascade.sh".  Use "--help" to determine options.  This file is generated during the mvn package/install process.
 * The cascade.sh tool does the following:

@@ Line 26: / Line 26: @@
 == Build and Install Cascade ==
-* Use eclipse or svn to check out each of these as top level projects from the [https://subversive.cims.nyu.edu/cascade/trunk/ svn repository].
+* Use eclipse or svn to check out each of these as top level projects from the [https://subversive.cims.nyu.edu/cascade/branches/wwang1109/cvc4_branch svn repository].
 ** c
 ** core

@@ Line 81: / Line 81: @@
 == Options ==
-Cascade provides a number of options, and we introduce the ones often be used. The complete list of them are attached in [[cascade_options]].
+Cascade provides a number of options, and here we only introduces those often be used. The complete list of them are attached in [[cascade_options]].
 * ''' -D, --debug''': run in debug mode.
 * '''--counter-example''': enable counter example generation when Cascade failed to prove.

@@ Line 173: / Line 173: @@
 indicates that root can reach NULL (which defines as 0 in [[list.c]]) finally, which means that the created list is an acyclic list.
-Another sample control file [[list_contains.ctrl]] is for the function contains(). Note that, the predicate '''_create_acyclic_list(f, root, length)''' is used to assume a list linked by field ''next'', with length 2 and starts with node root.
+Another sample control file [[list_contains.ctrl]] is for the function contains(). Note that, the predicate '''_create_acyclic_list(f, root, length)''' is used to assume the function parameter list with root as start node is created with length 2 and field ''next''.
-   __allocated_list(next, root, 2)
+   __create_acyclic_list(next, root, 2)

← Older revision		Revision as of 23:35, 17 December 2012
Line 172:		Line 172:
	_reach(next, root, 0)		_reach(next, root, 0)
	indicates that root can reach NULL (which defines as 0 in [[list.c]]) finally, which means that the created list is an acyclic list.		indicates that root can reach NULL (which defines as 0 in [[list.c]]) finally, which means that the created list is an acyclic list.
		+
		+	Another sample control file [[list_contains.ctrl]] is for the function contains(). Note that, the predicate '''_create_acyclic_list(f, root, length)''' is used here.
		+	__allocated_list(next, root, 2)
		+	It means a list with length 2 and starts with root has been created.

@@ Line 146: / Line 146: @@
 * Heap allocation predicate: '''_allocated(p, size)'''. It is used to assume that a region with size 4 has been allocated at p. This predicate is very helpful for modular verification, particularly of a function with pointers, arrays or structures as input arguments. As an example, consider [[strlen.c]] and [[strlen.ctrl]].
      _allocated(str, 4*sizeof(char))
-* Singly linked acyclic list creation predicate: '''_create_acyclic_list(f, root, length)'''. It means that a singly acyclic list with particular length and root has been created. This predicate is very helpful for modular verification of linked data structure manipulation functions, which takes linked lists as parameters.
+* Singly linked acyclic list creation predicate: '''_create_acyclic_list(f, root, length)'''. It is used to assume that a singly acyclic list with particular length and root has been created. This predicate is very helpful for modular verification of linked data structure manipulation functions, which takes linked lists as parameters.
      _create_acyclic_list(f, l1, 3)
 * Singly linked cyclic list creation predicate: '''_create_cyclic_list(f, root, length)'''.

@@ Line 148: / Line 148: @@
 * Singly acyclic list creation predicate: '''_create_acyclic_list(f, root, length)'''. It means that a singly acyclic list with particular length and root has been created. This predicate is very helpful for modular verification of linked data structure manipulation functions, which takes linked lists as parameters.
      _create_acyclic_list(f, l1, 3)
-* Singly cyclic list creation predicate '''_create_cyclic_list(f, root, length)'''.
+* Singly cyclic list creation predicate: '''_create_cyclic_list(f, root, length)'''.
      _create_cyclic_list(f, l2, 4)