@ -7,10 +7,12 @@
open ! IStd
open Ctl_parser_types
(* This module defines a language to define checkers. These checkers
are intepreted over the AST of the program . A checker is defined by a
CTL formula which express a condition saying when the checker should
report a problem * )
(* *
This module defines a language to define checkers . These checkers are interpreted over the AST of
the program . A checker is defined by a CTL formula which expresses a condition saying when the
checker should report a problem .
* )
(* * Transition labels used for example to switch from decl to stmt *)
type transitions =
@ -50,18 +52,13 @@ type t =
(* * EF phi <=> there exits a a path from the current node with a descendant where phi hold *)
| AG of transitions option * t (* * AG phi <=> for all discendant of the current node phi hold *)
| EG of transitions option * t
(* * EG phi <=>
there exists a path ( of descendants ) from the current node where phi hold at each node of the path * )
(* * EG phi <=> there exists a path ( of descendants ) from the current node where phi hold at each node of the path *)
| AU of transitions option * t * t
(* * AU ( phi1, phi2 ) <=>
for all paths from the current node phi1 holds in every node until ph2 holds * )
(* * AU ( phi1, phi2 ) <=> for all paths from the current node phi1 holds in every node until ph2 holds *)
| EU of transitions option * t * t
(* * EU ( phi1, phi2 ) <=>
there exists a path from the current node such that phi1 holds until phi2 holds * )
(* * EU ( phi1, phi2 ) <=> there exists a path from the current node such that phi1 holds until phi2 holds *)
| EH of ALVar . alexp list * t
(* * EH[classes]phi <=>
there exists a node defining a super class in the hierarchy of the class
defined by the current node ( if any ) where phi holds * )
(* * EH[classes]phi <=> there exists a node defining a super class in the hierarchy of the class defined by the current node ( if any ) where phi holds *)
| ET of ALVar . alexp list * transitions option * t
(* * ET [T] [l] phi <=> there exists a descentant an of the current node such that an is of type in set T
making a transition to a node an' via label l , such that in an phi holds . * )
@ -88,16 +85,13 @@ type t =
val equal : t -> t -> bool
type clause =
| CLet of ALVar . formula_id * ALVar . t list * t
(* Let clause: let id = definifion; *)
| CSet of ALVar . keyword * t
(* Set clause: set id = definition *)
| CDesc of ALVar . keyword * string
(* Description clause eg: set message = "..." *)
| CLet of ALVar . formula_id * ALVar . t list * t (* * Let clause: let id = definifion; *)
| CSet of ALVar . keyword * t (* * Set clause: set id = definition *)
| CDesc of ALVar . keyword * string (* * Description clause eg: set message = "..." *)
| CPath of [ ` WhitelistPath | ` BlacklistPath ] * ALVar . t list
type ctl_checker =
{ id : string ; (* Checker's id *) definitions : clause list ( * A list of let/set definitions *) }
{ id : string (* * Checker's id *) ; definitions : clause list ( * * A list of let/set definitions *) }
type al_file =
{ import_files : string list