diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml index 6bf70bfdb..f65622ba1 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml @@ -46,6 +46,7 @@ open Xsimplify open XprUtil (* cchlib *) +open CCHArithmeticConversion open CCHBasicTypes open CCHExternalPredicate open CCHFileContract @@ -1685,24 +1686,32 @@ object (self) ~ok:(fun ty1 -> TR.tfold ~ok:(fun ty2 -> - begin - match op with - | XPlus -> - Some (BinOp (PlusA, a1, a2, get_integer_promotion ty1 ty2)) - | XMinus -> - Some (BinOp (MinusA, a1, a2, get_integer_promotion ty1 ty2)) - | XMult -> - Some (BinOp (Mult, a1, a2, get_integer_promotion ty1 ty2)) - | XDiv -> - Some (BinOp (Div, a1, a2, get_integer_promotion ty1 ty2)) - | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1)) - | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1)) - | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool,[]))) - | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool,[]))) - | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool,[]))) - | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool,[]))) - | _ -> None - end) + TR.tfold + ~ok:(fun resulttyp -> + begin + match op with + | XPlus -> Some (BinOp (PlusA, a1, a2, resulttyp)) + | XMinus -> Some (BinOp (MinusA, a1, a2, resulttyp)) + | XMult -> Some (BinOp (Mult, a1, a2, resulttyp)) + | XDiv -> Some (BinOp (Div, a1, a2, resulttyp)) + | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1)) + | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1)) + | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, []))) + | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, []))) + | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, []))) + | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, []))) + | _ -> None + end) + ~error:(fun err -> + begin + log_diagnostics_result + ~tag:"x2api:integer-promotion" + ~msg:self#env#get_functionname + __FILE__ __LINE__ + [String.concat ", " err]; + None + end) + (usual_arithmetic_conversion ty1 ty2)) ~error:(fun err -> begin log_diagnostics_result diff --git a/CodeHawk/CHC/cchcil/cCHXParseFile.ml b/CodeHawk/CHC/cchcil/cCHXParseFile.ml index a6de253ea..b824a60e2 100644 --- a/CodeHawk/CHC/cchcil/cCHXParseFile.ml +++ b/CodeHawk/CHC/cchcil/cCHXParseFile.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny B. Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2026 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -72,6 +72,8 @@ let speclist = [ "directory to store the generated xml files"); ("-keep_system_includes", Arg.Unit (fun () -> keep_system_includes := true), "don't filter out functions in files with an absolute path name"); + ("-loglevel", Arg.String set_log_level, + "set level for logging (default: WARNING)"); ("-keepUnused", Arg.Set keepUnused, "keep unused type and function definitions")] @@ -263,7 +265,6 @@ let save_xml_file f = let main () = try let _ = read_args () in - let _ = set_log_level "DEBUG" in let _ = cildeclarations#set_filename !filename in let cilfile = Frontc.parse !filename () in let _ = log_info "Parsed %s [%s:%d]" !filename __FILE__ __LINE__ in diff --git a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml index 4dd890f59..6e7e764c6 100644 --- a/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml +++ b/CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml @@ -135,6 +135,8 @@ let speclist = [ "disable printing timing log messages"); ("-verbose", Arg.Unit (fun () -> system_settings#set_verbose true), "print status on proof obligations and invariants"); + ("-loglevel", Arg.String set_log_level, + "set level for logging (default: WARNING)"); ("-projectname", Arg.String system_settings#set_projectname, "name of the project (determines name of results directory)"); ("-keep_system_includes", @@ -166,7 +168,6 @@ let save_log_files (contenttype:string) = let main () = try - let _ = set_log_level "WARNING" in let _ = read_args () in let _ = chlog#set_max_entry_size 1000 in let _ = log_info "AIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAI" in diff --git a/CodeHawk/CHC/cchlib/Makefile b/CodeHawk/CHC/cchlib/Makefile index 1a710a38f..3a00d15b1 100644 --- a/CodeHawk/CHC/cchlib/Makefile +++ b/CodeHawk/CHC/cchlib/Makefile @@ -46,6 +46,7 @@ MLIS := \ cCHCodewalker \ cCHTypesSize \ cCHTypesUtil \ + cCHArithmeticConversion \ cCHBasicTypesXml \ cCHInterfaceDictionary \ cCHExternalPredicate \ @@ -74,6 +75,7 @@ SOURCES := \ cCHCodewalker \ cCHTypesSize \ cCHTypesUtil \ + cCHArithmeticConversion \ cCHBasicTypesXml \ cCHInterfaceDictionary \ cCHExternalPredicate \ diff --git a/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml new file mode 100644 index 000000000..691cfe79d --- /dev/null +++ b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml @@ -0,0 +1,128 @@ +(* ============================================================================= + CodeHawk C Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2005-2019 Kestrel Technology LLC + Copyright (c) 2020-2024 Henny B. Sipma + Copyright (c) 2024-2026 Aarno Labs LLC + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHLogger +open CHTraceResult + +(* cchlib *) +open CCHBasicTypes +open CCHTypesToPretty +open CCHUtilities + + +let p2s = CHPrettyUtil.pretty_to_string + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + +let get_integer_promotion (ty: typ): typ = + let promote_ikind (ik: ikind): ikind = + match ik with + | IChar | ISChar | IUChar | IShort | IBool -> IInt + | IUShort -> IUInt + | _ -> ik in + + match ty with + | TInt (ik, _) -> TInt (promote_ikind ik, []) + | TEnum (ename, _) -> + let einfo = CCHFileEnvironment.file_environment#get_enum ename in + TInt (promote_ikind einfo.ekind, []) + | _ -> + let _ = + log_diagnostics_result + ~tag:"get_integer_promotion: unexpected type" + __FILE__ __LINE__ + [p2s (typ_to_pretty ty)] in + ty + + +let usual_arithmetic_conversion (ty1: typ) (ty2: typ): typ traceresult = + + let convert_float (fk1: fkind) (fk2: fkind): fkind = + let is_complex (fk: fkind) = + match fk with + | FComplexLongDouble | FComplexDouble | FComplexFloat -> true + | _ -> false in + match fk1, fk2 with + | FComplexLongDouble, _ -> FComplexLongDouble + | _, FComplexLongDouble -> FComplexLongDouble + | FComplexDouble, _ -> FComplexDouble + | _, FComplexDouble -> FComplexDouble + | FComplexFloat, _ -> FComplexFloat + | _, FComplexFloat -> FComplexFloat + | FLongDouble, other when is_complex other -> FComplexLongDouble + | other, FLongDouble when is_complex other -> FComplexLongDouble + | FLongDouble, _ | _, FLongDouble -> FLongDouble + | FDouble, other when is_complex other -> FComplexDouble + | other, FDouble when is_complex other -> FComplexDouble + | FDouble, _ | _, FDouble -> FDouble + | FFloat, FFloat -> FFloat in + + let convert_int (ik1: ikind) (ik2: ikind): ikind = + match ik1, ik2 with + | IInt, ILong | ILong, IInt -> ILong + | IInt, ILongLong | ILongLong, IInt -> ILongLong + | ILong, ILongLong | ILongLong, ILong -> ILongLong + | IUInt, IULong | IULong, IUInt -> IULong + | _, IULongLong | IULongLong, _ -> IULongLong + | IInt, IUInt | IUInt, IInt -> IUInt + | ILong, IULong | IULong, ILong -> IULong + | IInt, IULong | IULong, IInt -> IULong + | ILong, IUInt | IUInt, ILong -> ILong + | ILongLong, IUInt | IUInt, ILongLong -> ILongLong + | IUInt128, _ | _, IUInt128 -> IUInt128 + | IInt128, _ | _, IInt128 -> IInt128 + | _ -> + (* this should not happen *) + raise + (CCHFailure + (LBLOCK [ + STR "Missing case in integer promotion: "; + STR (int_type_to_string ik1); + STR " and "; + STR (int_type_to_string ik2)])) in + + match ty1, ty2 with + | TFloat (fk1, _), TFloat (fk2, _) -> Ok (TFloat (convert_float fk1 fk2, [])) + | TFloat _, _ -> Ok ty1 + | _, TFloat _ -> Ok ty2 + | _ -> + let pty1 = get_integer_promotion ty1 in + let pty2 = get_integer_promotion ty2 in + match pty1, pty2 with + | TInt (ik1, _), TInt (ik2, _) when ik1 = ik2 -> Ok (TInt (ik1, [])) + | TInt (ik1, _), TInt (ik2, _) -> Ok (TInt (convert_int ik1 ik2, [])) + | _ -> + Error [(elocm __LINE__) + ^ "not an arithmetic type: " + ^ (p2s (typ_to_pretty ty1)) + ^ " or " + ^ (p2s (typ_to_pretty ty2))] diff --git a/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli new file mode 100644 index 000000000..0334fe53a --- /dev/null +++ b/CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli @@ -0,0 +1,113 @@ +(* ============================================================================= + CodeHawk C Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2005-2019 Kestrel Technology LLC + Copyright (c) 2020-2024 Henny B. Sipma + Copyright (c) 2024-2026 Aarno Labs LLC + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHTraceResult + +(* cchlib *) +open CCHBasicTypes + +(** The Usual Arithmetic Conversions (C Standard 6.3.1.8) + + All of the usual arithmetic conversions applied to expressions in the C + source code are supplied by the CIL parser in the form of casts. + + The implementation in this file serves to determine the result type of an + expression constructed to serve as a precondition or side effect to a + function. + *) + + +(** {1 Integer promotion: C Standard 6.3.1.1} + + The following may be used in an expression wherever an int or unsigned + int may be used: + - an object or expression with an integer type whose integer conversion + rank is less than or equal to the rank of int and unsigned int. + - a bit-field of type _Bool, int, signed int, unsigned int. + + If an int can represent all values of the original type, the value is + converted to an int; otherwise it is converted to an unsigned int. These + are called the integer promotions. All other types are unchanged by the + integer promotions. + + The integer promotions preserve value including sign. + *) + +val get_integer_promotion: typ -> typ + + +(** {1 Usual arithmetic conversions: C Standard 6.3.1.8} + + Many operators that expect operands of arithmetic type cause conversions + and yield result types in a similar way. The purpose is to determine a + common real type for the operands and result. For the specified operands, + each operand is converted, without change of type domain, to a type whose + corresponding real type is the common real type. Unless explicitly stated + otherwise, the common real type is also the corresponding real type of + the result, whose type domain is the type domain of the operands if they + are the same, and complex otherwise. This pattern is called 'the usual + arithmetic conversions'. + + First, if the corresponding real type of either operand is long double, + the other operand is converted, without change of type domain, to a type + whose corresponding real type is long double. + + Otherwise, if the corresponding real type of either operand is double, the + other operand is converted, without change of type domain, to a type + whose corresponding real type is double. + + Otherwise, if the corresponding real type of either operand is float, the + other operand is converted, without change of type domain, to a type whose + corresponding type is float. + + Other, the integer promotions are performed on both operands. Then the + following rules are applied to the promoted operands: + + If both operands have the same type, then no further conversion is needed. + + Otherwise, if both operands have signed integer types or both have unsigned + integer types, the operand with the type of lesser integer conversion rank + is converted to the type of the operand with greater rank. + + Otherwise, if the operand that has unsigned integer type has rank greater + or equal to the rank of the type of the other operand, then the operand + with signed integer type is converted to the type of the operand with + unsigned integer type. + + Otherwise, if the type of the operand with signed integer type can represent + all of the values of the type of the operand with unsigned integer type, then + the operand with unsigned integer type is converted to the type of the operand + with signed integer type. + + Otherwise, both operands are converted to the unsigned integer type + corresponding to the type of the operand with signed integer type. + *) + +val usual_arithmetic_conversion: typ -> typ -> typ traceresult diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml index 7f0fde095..d4346feec 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml @@ -418,90 +418,6 @@ let is_longlong ik = match ik with ILongLong | IULongLong -> true | _ -> false -(** {1 Integer promotion: C Standard 6.3.1.1, 6.3.1.8} - - The following may be used in an expression wherever an int or unsigned - int may be used: - - an object or expression with an integer type whose integer conversion - rank is less than or equal to the rank of int and unsigned int. - - a bit-field of type _Bool, int, signed int, unsigned int. - - If an int can represent all values of the original type, the value is - converted to an int; otherwise it is converted to an unsigned int. These - are called the integer promotions. A - - First, both types are promoted to either signed or unsigned int. - - If both operands have the same type, then no further conversion is needed. - - Otherwise, if both operands have signed integer types or both have unsigned - integer types, the operand with the type of lesser integer conversion rank - is converted to the type of the operand with greater rank. - - Otherwise, if the operand that has unsigned integer type has rank greater - or equal to the rank of the type of the other operand, then the operand - with signed integer type is converted to the type of the operand with - unsigned integer type. - - Otherwise, if the type of the operand with signed integer type can represent - all of the values of the type of the operand with unsigned integer type, then - the operand with unsigned integer type is converted to the type of the operand - with signed integer type. - - Otherwise, both operands are converted to the unsigned integer type - corresponding to the type of the operand with signed integer type. - *) - -let get_integer_promotion (ty1: typ) (ty2: typ): typ = - let promote_ikind (ik: ikind): ikind = - match ik with - | IChar | ISChar | IUChar | IShort | IBool -> IInt - | IUShort -> IUInt - | _ -> ik in - let promote_type (ty: typ): ikind = - match ty with - | TInt (ik, _) -> promote_ikind ik - | TEnum (ename, _) -> - let einfo = CCHFileEnvironment.file_environment#get_enum ename in - promote_ikind einfo.ekind - | _ -> - raise - (CCHFailure - (LBLOCK [ - STR "Unexpected types for integer promotion: "; - typ_to_pretty ty1])) in - let usual_arithmetic_conversion (ik1: ikind) (ik2: ikind): ikind = - match (ik1, ik2) with - | (IInt, ILong) | (ILong, IInt) -> ILong - | (IInt, ILongLong) | (ILongLong, IInt) -> ILongLong - | (ILong, ILongLong) | (ILongLong, ILong) -> ILongLong - | (IUInt, IULong) | (IULong, IUInt) -> IULong - | (_, IULongLong) | (IULongLong, _) -> IULongLong - | (IInt, IUInt) | (IUInt, IInt) -> IUInt - | (ILong, IULong) | (IULong, ILong) -> IULong - | (IInt, IULong) | (IULong, IInt) -> IULong - | (ILong, IUInt) | (IUInt, ILong) -> ILong - | (ILongLong, IUInt) | (IUInt, ILongLong) -> ILongLong - | (IUInt128, _) | (_, IUInt128) -> IUInt128 - | (IInt128, _) | (_, IInt128) -> IInt128 - | _ -> - raise - (CCHFailure - (LBLOCK [ - STR "Missing case in integer promotion: "; - STR (int_type_to_string ik1); - STR " and "; - STR (int_type_to_string ik2)])) in - let ik1 = promote_type ty1 in - let ik2 = promote_type ty2 in - let result_ik = - if ik1 = ik2 then - ik1 - else - usual_arithmetic_conversion ik1 ik2 in - TInt (result_ik, []) - - let rec get_field_offset offset = match offset with | NoOffset -> diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli index 581eeba0e..28eaa363c 100644 --- a/CodeHawk/CHC/cchlib/cCHTypesUtil.mli +++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.mli @@ -65,8 +65,6 @@ val is_unsigned_type: ikind -> bool val is_character_type: ikind -> bool -val get_integer_promotion: typ -> typ -> typ - val ikind_size_leq : ikind -> ikind -> bool val const_fits_kind: constant -> ikind -> bool diff --git a/CodeHawk/CHC/cchlib/cCHVersion.ml b/CodeHawk/CHC/cchlib/cCHVersion.ml index a2f556dd2..e5e90caae 100644 --- a/CodeHawk/CHC/cchlib/cCHVersion.ml +++ b/CodeHawk/CHC/cchlib/cCHVersion.ml @@ -62,5 +62,5 @@ object (self) end let version = new version_info_t - ~version:"0.3.0_20260604" - ~date:"2026-06-04" + ~version:"0.3.0_20260606" + ~date:"2026-06-06" diff --git a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml index b326deab3..ae2b213dc 100644 --- a/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml +++ b/CodeHawk/CHC/cchpre/cCHPrimaryProofObligations.ml @@ -39,6 +39,7 @@ open CHTraceResult open CHUtil (* cchlib *) +open CCHArithmeticConversion open CCHBasicTypes open CCHContext open CCHDictionary @@ -283,12 +284,12 @@ and create_po_binop | Shiftlt | Shiftrt -> (* result is undefined if second operand is negative or if second operand - is greater than or equal to the width of the first operand, + is greater than or equal to the width of the promoted left operand, ref. C99:6.5.7(3) *) begin match fenv#get_type_unrolled t with | TInt (ik,_) -> - let ty = get_integer_promotion (TInt (ik,[])) (TInt (IInt,[])) in + let ty = get_integer_promotion (TInt (ik, [])) in begin match ty with | TInt (ikp,_) -> diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile index f8cd3ccc4..cde3ad979 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile @@ -58,7 +58,7 @@ SOURCES := \ OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx)) -all: make_dirs cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest +all: make_dirs cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest doc: @@ -66,17 +66,13 @@ make_dirs: @mkdir -p cmx @mkdir -p cmi -cCHPOCheckInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckInitializedTest.cmi cmx/cCHPOCheckInitializedTest.cmx - $(CAMLLINK) -o cCHPOCheckInitializedTest $(OBJECTS) cmx/cCHPOCheckInitializedTest.cmx - cCHPOCheckLocallyInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckLocallyInitializedTest.cmi cmx/cCHPOCheckLocallyInitializedTest.cmx $(CAMLLINK) -o cCHPOCheckLocallyInitializedTest $(OBJECTS) cmx/cCHPOCheckLocallyInitializedTest.cmx cCHPOCheckOutputParameterInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckOutputParameterInitializedTest.cmi cmx/cCHPOCheckOutputParameterInitializedTest.cmx $(CAMLLINK) -o cCHPOCheckOutputParameterInitializedTest $(OBJECTS) cmx/cCHPOCheckOutputParameterInitializedTest.cmx -run: cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest - ./cCHPOCheckInitializedTest +run: cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest ./cCHPOCheckLocallyInitializedTest ./cCHPOCheckOutputParameterInitializedTest @@ -100,6 +96,5 @@ clean: rm -f *.ml~ rm -f *.mli~ rm -f Makefile~ - rm -f cCHPOCheckInitializedTest rm -f cCHPOCheckLocallyInitializedTest rm -f cCHPOCheckOutputParameterInitialized diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml deleted file mode 100644 index 4f7b68935..000000000 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* ============================================================================= - CodeHawk Unit Testing Framework - Author: Henny Sipma - Adapted from: Kaputt (https://kaputt.x9c.fr/index.html) - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2025 Aarno Labs LLC - - Permission is hereby granted, free of charge, to any person obtaining a copy - of this software and associated documentation files (the "Software"), to deal - in the Software without restriction, including without limitation the rights - to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - copies of the Software, and to permit persons to whom the Software is - furnished to do so, subject to the following conditions: - - The above copyright notice and this permission notice shall be included in all - copies or substantial portions of the Software. - - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) - -open CCHPreTypes -open CCHProofScaffolding - -module A = TCHAssertion -module TS = TCHTestSuite -module CA = TCHCchanalyzeAssertion -module CU = TCHCchanalyzeUtils - - -let testname = "cCHPOCheckInitializedTest" -let lastupdated = "2025-11-10" - - -let po_filter (po: proof_obligation_int): proof_obligation_int option = - match po#get_predicate with - | PInitialized _ -> Some po - | _ -> None - - -(* See CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.mli - for a description and example of how to specify the tests. - - Tests: - - Test: gl-inv-001: - ================= - int gl_inv_001(void) { - - int i = 5; - - return i; - } - - Test: gl-inv-002: - ================= - typedef struct mystruct_s { - int fld1; - int fld2; - } mystruct; - - - int gl_inv_002(void) { - - mystruct s = {.fld1 = 5, .fld2 = 3 }; - - return s.fld1; - } - - Test: gl-inv-003: - ================= - int gl_inv_003(int k) { - - int i; - - if (k > 0) { - i = 5; - } else { - i = 3; - } - - return i; - } - - Test gl-inv-xpr-001: - ==================== - int gl_inv_xpr_001(void) { - - int i = 5; - - int *p = &i; - - return *p; - } - - - *) -let check_safe () = - let tests = [ - ("gl-inv-001", - "gl_inv_001", "gl_inv_001", - [], -1, -1, - Some "inv_implies_safe", "assignedAt#5"); - ("gl-inv-002", - "gl_inv_002", "gl_inv_002", - [], -1, -1, - Some "inv_implies_safe", "assignedAt#11"); - ("gl-inv-003", - "gl_inv_003", "gl_inv_003", - [], 14, -1, - Some "inv_implies_safe", "") - (* disabling the tests based on the presence of an - initial value - ("gl-inv-xpr-001", - "gl_inv_xpr_001", "gl_inv_xpr_001", - ["(*p)"], -1, -1, - "inv_xpr_implies_safe", "variable (*p) has the value 5"); - ("gl-inv-xpr-002", - "gl_inv_xpr_002", "gl_inv_xpr_002", - ["(*p)"], -1, -1, - "inv_xpr_implies_safe", "variable (*p) has the value 8"); - ("gl-inv-xpr-003", - "gl_inv_xpr_003", "gl_inv_xpr_003", - [], 11, -1, - "inv_xpr_implies_safe", "variable i has the value 8"); - ("gl-inv-bounded-xpr-001", - "gl_inv_bounded_xpr_001", "gl_inv_bounded_xpr_001", - ["(*p)"], 14, -1, - "inv_bounded_xpr_implies_safe", "variable (*p) is bounded by LB: 3 and UB: 5"); - ("gl-stackvar-001", - "gl_stackvar_001", "gl_stackvar_001", - ["(*p)"], 14, -1, - "memlval_vinv_memref_stackvar_implies_safe", - "assignment(s) to i: assignedAt#11_xx_assignedAt#9") - *) - ] in - begin - TS.new_testsuite (testname ^ "_check_safe") lastupdated; - CHTiming.disable_timing (); - - List.iter - (fun (title, filename, funname, reqargs, line, byte, xdetail, expl) -> - TS.add_simple_test - ~title - (fun () -> - let _ = CCHSettings.system_settings#set_undefined_behavior_analysis in - let _ = CU.analysis_setup "PInitialized" filename in - let po_s = proof_scaffolding#get_proof_obligations funname in - let po_s = List.filter_map po_filter po_s in - let tgtpo_o = CU.select_target_po ~reqargs ~line ~byte po_s in - begin - CU.analysis_take_down filename; - match tgtpo_o with - | Some po -> CA.expect_safe_detail ~po ~xdetail ~expl () - | _ -> - let s_po_s = List.map CU.located_po_to_string po_s in - A.fail_msg - ("Unable to uniquely select target proof obligation: " - ^ "[" - ^ (String.concat "; " s_po_s) - ^ "]") - end - ) - ) tests; - - TS.launch_tests() - end - - -let () = - begin - TS.new_testfile testname lastupdated; - check_safe (); - TS.exit_file () - end diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli deleted file mode 100644 index 25735d4d3..000000000 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* ============================================================================= - CodeHawk Unit Testing Framework - Author: Henny Sipma - Adapted from: Kaputt (https://kaputt.x9c.fr/index.html) - ------------------------------------------------------------------------------ - The MIT License (MIT) - - Copyright (c) 2025 Aarno Labs LLC - - Permission is hereby granted, free of charge, to any person obtaining a copy - of this software and associated documentation files (the "Software"), to deal - in the Software without restriction, including without limitation the rights - to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - copies of the Software, and to permit persons to whom the Software is - furnished to do so, subject to the following conditions: - - The above copyright notice and this permission notice shall be included in all - copies or substantial portions of the Software. - - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. - ============================================================================= *) diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune index e7231e3c3..2fd1fcbe6 100644 --- a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune +++ b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/dune @@ -1,19 +1,10 @@ (tests (names - cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest cCHPOCheckOutputParameterInitializedTest cCHPOCheckErrnoWrittenTest ) (deps - testinputs/PInitialized/gl_inv_001.cch.tar.gz - testinputs/PInitialized/gl_inv_002.cch.tar.gz - testinputs/PInitialized/gl_inv_003.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz - testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz - testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz - testinputs/PInitialized/gl_stackvar_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_gl_inv_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_gl_memlval_memref_001.cch.tar.gz testinputs/PLocallyInitialized/locally_initialized_rl_xpr_001.cch.tar.gz diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz deleted file mode 100644 index 103afd723..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_001.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz deleted file mode 100644 index 979ba648e..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_002.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_003.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_003.cch.tar.gz deleted file mode 100644 index 7f21b510a..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_003.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz deleted file mode 100644 index a2df32a7d..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_bounded_xpr_001.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz deleted file mode 100644 index be90d78c2..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_001.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz deleted file mode 100644 index c694e880f..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_002.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz deleted file mode 100644 index 1bad88dbb..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_inv_xpr_003.cch.tar.gz and /dev/null differ diff --git a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz b/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz deleted file mode 100644 index ef540af26..000000000 Binary files a/CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/testinputs/PInitialized/gl_stackvar_001.cch.tar.gz and /dev/null differ