User Tools

Site Tools


cprover_beginner_s_guide

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
cprover_beginner_s_guide [2015/06/09 13:24]
bjowac
cprover_beginner_s_guide [2017/07/15 12:14] (current)
kroening
Line 110: Line 110:
 {{anchor|util}} {{anchor|util}}
  
-[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​|util/​]] contains the low-level data structures and manipulation functions that+[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​|util/​]] contains the low-level data structures and manipulation functions that
 are used through-out the CPROVER code-base. For almost any low-level task, are used through-out the CPROVER code-base. For almost any low-level task,
 the code required is probably in util/. Key files include: the code required is probably in util/. Key files include:
Line 124: Line 124:
 of exprt should be used. of exprt should be used.
  
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​irep.h|irep.h]]** This contains the definition of irept, the basis of many of the data structures in the project. They should not be used directly; one of the derived classes should be used. For more information see Section [[cprover_beginner_s_guide#​irept/​|irept/​]]. +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​irep.h|irep.h]]** This contains the definition of irept, the basis of many of the data structures in the project. They should not be used directly; one of the derived classes should be used. For more information see Section [[cprover_beginner_s_guide#​irept/​|irept/​]]. 
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​expr.h|expr.h]]** The parent class for all of the expressions. Provides a number of generic functions, exprt can be used with these but when creating data, subclasses of exprt should be used. +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​expr.h|expr.h]]** The parent class for all of the expressions. Provides a number of generic functions, exprt can be used with these but when creating data, subclasses of exprt should be used. 
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​std_expr.h|std_expr.h]]** Provides subclasses of exprt for common kinds of expression for example plus exprt, minus exprt, dereference exprt. These are the intended interface for creating expressions.  +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​std_expr.h|std_expr.h]]** Provides subclasses of exprt for common kinds of expression for example plus exprt, minus exprt, dereference exprt. These are the intended interface for creating expressions.  
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​std_types.h|std_types.h]]** Provides subclasses of typet (a subclass of irept) to model C and C++ types. This is one of the preferred interfaces to irept. The front-ends handle type promotion and most coercision so the type system and checking goto-programs is simpler than C. +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​std_types.h|std_types.h]]** Provides subclasses of typet (a subclass of irept) to model C and C++ types. This is one of the preferred interfaces to irept. The front-ends handle type promotion and most coercision so the type system and checking goto-programs is simpler than C. 
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​dstring.h|dstring.h]]** The CPROVER string class. This enables sharing between strings which significantly reduces the amount of memory required and speeds comparison. dstring should not be used directly, irep idt should be+  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​dstring.h|dstring.h]]** The CPROVER string class. This enables sharing between strings which significantly reduces the amount of memory required and speeds comparison. dstring should not be used directly, irep idt should be
 used instead, which (dependent on build options) is an alias for dstring. ​ used instead, which (dependent on build options) is an alias for dstring. ​
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​mp_arith.h|mp_arith.h]]** The wrapper class for multi-precision arithmetic within CPROVER. Also see arith tools.h. +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​mp_arith.h|mp_arith.h]]** The wrapper class for multi-precision arithmetic within CPROVER. Also see arith tools.h. 
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​ieee_float.h|ieee_float.h]]** The arbitrary precision float model used within CPROVER. Based on mp_integers.  +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​ieee_float.h|ieee_float.h]]** The arbitrary precision float model used within CPROVER. Based on mp_integers.  
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​context.h|context.h]]** A generic container for symbol table like constructs such as namespaces. Lookup gives type, location of declaration,​ name, ‘pretty name’, whether it is static or not.  +  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​context.h|context.h]]** A generic container for symbol table like constructs such as namespaces. Lookup gives type, location of declaration,​ name, ‘pretty name’, whether it is static or not.  
-  * **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​util/​namespace.h|namespace.h]]** The preferred interface for the context class. The key function is lookup which converts a string (irep idt) to a symbol which gives the scope of declaration,​ type and so on. This works for functions as well as variables.+  * **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​util/​namespace.h|namespace.h]]** The preferred interface for the context class. The key function is lookup which converts a string (irep idt) to a symbol which gives the scope of declaration,​ type and so on. This works for functions as well as variables.
  
 === langapi/ === === langapi/ ===
Line 144: Line 144:
 === ansi-c/ === === ansi-c/ ===
  
-**[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​ansi-c|ansi-c/​]]**+**[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​ansi-c|ansi-c/​]]**
 contains the front-end for ANSI C, plus a variety of common extensions. This contains the front-end for ANSI C, plus a variety of common extensions. This
 parses the file, performs some basic sanity checks (this is one area in which the UI parses the file, performs some basic sanity checks (this is one area in which the UI
Line 161: Line 161:
 === cpp/ === === cpp/ ===
  
-The directory **[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​cpp|cpp/​]]** contains the C++ front-end. ​+The directory **[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​cpp|cpp/​]]** contains the C++ front-end. ​
 It supports the subset of C++ commonly found in embedded and system applications. Consequentially it doesn’t It supports the subset of C++ commonly found in embedded and system applications. Consequentially it doesn’t
 have full support for templates and many of the more advanced and obscure have full support for templates and many of the more advanced and obscure
Line 173: Line 173:
  
  
-**[[http://www.cprover.org/​svn/​cbmc/​trunk/​src/​goto-programs/​|Goto programs]]** ​+**[[http://svn.cprover.org/​svn/​cbmc/​trunk/​src/​goto-programs/​|Goto programs]]** ​
 are the intermediate representation of the CPROVER tool chain. are the intermediate representation of the CPROVER tool chain.
 They are language independent and similar to many of the compiler intermedi- They are language independent and similar to many of the compiler intermedi-
Line 440: Line 440:
 by incoming edges. Finally instructiont have informational function and by incoming edges. Finally instructiont have informational function and
 location fields that indicate where they are in the code. location fields that indicate where they are in the code.
- 
  
cprover_beginner_s_guide.txt · Last modified: 2017/07/15 12:14 by kroening