Preconditions

CodeHawk/CH/chutil/cHUtil.ml

@@ -174,6 +174,17 @@ let list_split_p (p:'a -> bool) (l:'a list):('a list * 'a list) =
   loop [] [] l
 
 
+let list_slice (lst: 'a list) (index: int) (count:int): 'a list option  =
+  if index < 0 || count < 0 || (List.length lst) < index + count then
+    None
+  else
+    let rec aux l i n result =
+      if i > 0 then aux (List.tl l) (i-1) n result
+      else if n > 0 then aux (List.tl l) 0 (n-1) ((List.hd l) :: result)
+      else List.rev result in
+    Some (aux lst index count [])
+
+
 let list_suffix (n:int) (l:'a list) =
   let rec aux n l =
     match l with

CodeHawk/CH/chutil/cHUtil.mli

@@ -60,6 +60,13 @@ val list_split_p: ('a -> bool) -> 'a list -> ('a list * 'a list)
 
 val list_sub: 'a list -> int -> int -> 'a list
 
+(** [list_slice lst index count] returns a list of [count] elements from [st]
+    starting at [index] (counting from zero).
+
+    Returns None if [index] or [count] are negative, or if [lst] does not
+    include sufficient elements to fill the slice. *)
+val list_slice: 'a list -> int -> int -> 'a list option
+
 val list_suffix: int -> 'a list -> 'a list
 
 val list_maxf: 'a list -> ('a -> 'a -> int) -> 'a
@@ -84,7 +91,7 @@ val pair_compare:
   ('a * 'b) -> ('a * 'b) -> ('a -> 'a -> int) -> ('b -> 'b -> int) -> int
 
 
-  (** [triple_compare t1 t2 returns the result of the element-wise comparison
+  (** [triple_compare t1 t2] returns the result of the element-wise comparison
       of triples [t1] and [t2], using [f1], [f2], and [f3] as comparison
       functions for the three elements, respectively.*)
 val triple_compare:

CodeHawk/CHB/bchlib/Makefile

@@ -82,7 +82,7 @@ MLIS := \
 	bCHPrecondition \
 	bCHPostcondition \
 	bCHSideeffect \
-	bCHBCAttributes \
+	bCHAttributesFunctionSemantics \
 	bCHFunctionSemantics \
 	bCHFunctionSummary \
 	bCHVariable \
@@ -111,6 +111,8 @@ MLIS := \
 	bCHCallSemanticsRecorder \
 	bCHFloc \
 	bCHCallgraph \
+	bCHFunctionPODischarge \
+	bCHFunctionSemanticsAttributes \
 	bCHMetricsHandler \
 	bCHDisassemblySummary \
 	bCHMetrics \
@@ -175,7 +177,7 @@ SOURCES := \
 	bCHPrecondition \
 	bCHPostcondition \
 	bCHSideeffect \
-	bCHBCAttributes \
+	bCHAttributesFunctionSemantics \
 	bCHFunctionSemantics \
 	bCHFunctionSummary \
 	bCHVariable \
@@ -204,6 +206,8 @@ SOURCES := \
 	bCHCallSemanticsRecorder \
 	bCHFloc \
 	bCHCallgraph \
+	bCHFunctionPODischarge \
+	bCHFunctionSemanticsAttributes \
 	bCHMetricsHandler \
 	bCHDisassemblySummary \
 	bCHMetrics \