Merge branch 'diffblue:develop' into develop

Author: yvizel

.github/workflows/pull-request-check-clang-format.sh

@@ -7,7 +7,7 @@ set -e
 echo "Pull request's base branch is: ${BASE_BRANCH}"
 echo "Pull request's merge branch is: ${MERGE_BRANCH}"
 echo "Pull request's source branch is: ${GITHUB_HEAD_REF}"
-clang-format-11 --version
+clang-format-15 --version
 
 # The checkout action leaves us in detatched head state. The following line
 # names the checked out commit, for simpler reference later.
@@ -26,7 +26,7 @@ echo "Checking for formatting errors introduced since $MERGE_BASE"
 
 # Do the checking. "eval" is used so that quotes (as inserted into $EXCLUDES
 # above) are not interpreted as parts of file names.
-eval git-clang-format-11 --binary clang-format-11 $MERGE_BASE -- $EXCLUDES
+eval git-clang-format-15 --binary clang-format-15 $MERGE_BASE -- $EXCLUDES
 git diff > formatted.diff
 if [[ -s formatted.diff ]] ; then
   echo 'Formatting error! The following diff shows the required changes'

.github/workflows/syntax-checks.yaml

@@ -6,7 +6,7 @@ on:
 jobs:
   # This job takes approximately 1 minute
   check-clang-format:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v4
         with:
@@ -19,8 +19,8 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq clang-format-11
-      - name: Check updated lines of code match clang-format-11 style
+          sudo apt-get install --no-install-recommends -yq clang-format-15
+      - name: Check updated lines of code match clang-format-15 style
         env:
           BASE_BRANCH: ${{ github.base_ref }}
           MERGE_BRANCH: ${{ github.ref }}

CODING_STANDARD.md

@@ -340,14 +340,13 @@ Now, you can commit and push the formatting fixes.
 To avoid waiting until you've made a PR to find formatting issues, you can
 install clang-format locally and run it against your code as you are working.
 
-Different versions of clang-format have slightly different behaviors. CBMC uses
-clang-format-11 as it is available the repositories for Ubuntu 20.04 and
-Homebrew.
-To install on a Unix-like system, try installing using the system package
-manager:
+Different versions of clang-format have slightly different behaviors.  CBMC
+uses clang-format-15, or later, available in the standard Ubuntu 24.04 and
+Homebrew repositories.  To install on a Unix-like system, try installing
+using the system package manager:
 ```
-apt-get install clang-format-11  # Run this on Ubuntu, Debian etc.
-brew install clang-format@11     # Run this on a Mac with Homebrew installed
+apt-get install clang-format     # Run this on Ubuntu, Debian etc.
+brew install clang-format        # Run this on a Mac with Homebrew installed
 ```
 
 If your platform doesn't have a package for clang-format, you can download a

regression/ansi-c/errors/file_with_no_newline.desc

@@ -0,0 +1,7 @@
+CORE
+file_with_no_newline.i
+
+^file_with_no_newline\.i((:[01]:1)|(\(1\))): error: .*$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--

regression/ansi-c/errors/file_with_no_newline.i

@@ -0,0 +1 @@
+syntax error, no newline here ->

regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/main.c

@@ -0,0 +1,21 @@
+#pragma pack(push)
+#pragma pack(1)
+typedef struct
+{
+  int data[2];
+} arr;
+
+typedef struct
+{
+  arr vec[2];
+} arrvec;
+#pragma pack(pop)
+
+int main()
+{
+  arrvec A;
+  arrvec *x = &A;
+  __CPROVER_assume(x->vec[1].data[0] < 42);
+  unsigned k;
+  __CPROVER_assert(k != 2 || ((int *)x)[k] < 42, "");
+}

regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/main.c

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE no-new-smt
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/__sort_of_CPROVER_round_to_integralf-01/test.desc

@@ -3,9 +3,8 @@ access.c
 --program-only
 ^EXIT=0$
 ^SIGNAL=0$
-s!0@1#2\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+s!0@1#2\.\.n ==.*\{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] \}
 --
-byte_update
 --
 This tests applying field-sensitivity to a pointer to an array that is part of a struct. See cbmc issue #5397 and PR #5418 for more detail.
 Disabled for paths-lifo mode, which does not support --program-only.

regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/main.c

@@ -0,0 +1,92 @@
+(set-logic FP)
+
+(define-fun zero () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 0))
+(define-fun minus-zero () (_ FloatingPoint 11 53) (fp.neg zero))
+(define-fun one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 1))
+(define-fun minus-one () (_ FloatingPoint 11 53) (fp.neg one))
+(define-fun zero-point-one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 0.1))
+(define-fun minus-zero-point-one () (_ FloatingPoint 11 53) (fp.neg zero-point-one))
+(define-fun ten-point-one () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 10.1))
+(define-fun minus-ten-point-one () (_ FloatingPoint 11 53) (fp.neg ten-point-one))
+(define-fun ten () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 10))
+(define-fun minus-ten () (_ FloatingPoint 11 53) (fp.neg ten))
+(define-fun eleven () (_ FloatingPoint 11 53) ((_ to_fp 11 53) RNE 11))
+(define-fun minus-eleven () (_ FloatingPoint 11 53) (fp.neg eleven))
+(define-fun magic () (_ FloatingPoint 11 53) (fp #b0 #b10000110011 #x0000000000000))
+(define-fun dmax () (_ FloatingPoint 11 53) (fp #b0 #b11111111110 #xFFFFFFFFFFFFF))
+
+(assert (not (and
+
+  ; round up
+  (= (fp.roundToIntegral RTP (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTP (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTP (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTP zero) zero)
+  (= (fp.roundToIntegral RTP minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTP one) one)
+  (= (fp.roundToIntegral RTP zero-point-one) one)
+  (= (fp.roundToIntegral RTP minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RTP ten-point-one) eleven)
+  (= (fp.roundToIntegral RTP minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RTP magic) magic)
+  (= (fp.roundToIntegral RTP dmax) dmax)
+
+  ; round down
+  (= (fp.roundToIntegral RTN (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTN (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTN (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTN zero) zero)
+  (= (fp.roundToIntegral RTN minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTN one) one)
+  (= (fp.roundToIntegral RTN zero-point-one) zero)
+  (= (fp.roundToIntegral RTN minus-zero-point-one) minus-one)
+  (= (fp.roundToIntegral RTN ten-point-one) ten)
+  (= (fp.roundToIntegral RTN minus-ten-point-one) minus-eleven)
+  (= (fp.roundToIntegral RTN magic) magic)
+  (= (fp.roundToIntegral RTN dmax) dmax)
+
+  ; round to nearest ties to even
+  (= (fp.roundToIntegral RNE (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RNE (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RNE (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RNE zero) zero)
+  (= (fp.roundToIntegral RNE minus-zero) minus-zero)
+  (= (fp.roundToIntegral RNE one) one)
+  (= (fp.roundToIntegral RNE zero-point-one) zero)
+  (= (fp.roundToIntegral RNE minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RNE ten-point-one) ten)
+  (= (fp.roundToIntegral RNE minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RNE magic) magic)
+  (= (fp.roundToIntegral RNE dmax) dmax)
+
+  ; round to zero
+  (= (fp.roundToIntegral RTZ (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RTZ (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RTZ (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RTZ zero) zero)
+  (= (fp.roundToIntegral RTZ minus-zero) minus-zero)
+  (= (fp.roundToIntegral RTZ one) one)
+  (= (fp.roundToIntegral RTZ zero-point-one) zero)
+  (= (fp.roundToIntegral RTZ minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RTZ ten-point-one) ten)
+  (= (fp.roundToIntegral RTZ minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RTZ magic) magic)
+  (= (fp.roundToIntegral RTZ dmax) dmax)
+
+  ; round to nearest ties to away
+  (= (fp.roundToIntegral RNA (_ NaN 11 53)) (_ NaN 11 53))
+  (= (fp.roundToIntegral RNA (_ +oo 11 53)) (_ +oo 11 53))
+  (= (fp.roundToIntegral RNA (_ -oo 11 53)) (_ -oo 11 53))
+  (= (fp.roundToIntegral RNA zero) zero)
+  (= (fp.roundToIntegral RNA minus-zero) minus-zero)
+  (= (fp.roundToIntegral RNA one) one)
+  (= (fp.roundToIntegral RNA zero-point-one) zero)
+  (= (fp.roundToIntegral RNA minus-zero-point-one) minus-zero)
+  (= (fp.roundToIntegral RNA ten-point-one) ten)
+  (= (fp.roundToIntegral RNA minus-ten-point-one) minus-ten)
+  (= (fp.roundToIntegral RNA magic) magic)
+  (= (fp.roundToIntegral RNA dmax) dmax)
+)))
+
+; should be unsat
+(check-sat)

regression/cbmc-library/__sort_of_CPROVER_round_to_integrall-01/test.desc

@@ -208,13 +208,13 @@ void ansi_c_parsert::set_pragma_cprover()
     for(const auto &pragma : pragma_set)
       flattened[pragma.first] = pragma.second;
 
-  source_location.remove(ID_pragma);
+  _source_location.remove(ID_pragma);
 
   for(const auto &pragma : flattened)
   {
     std::string check_name = id2string(pragma.first);
     std::string full_name =
       (pragma.second ? "enable:" : "disable:") + check_name;
-    source_location.add_pragma(full_name);
+    _source_location.add_pragma(full_name);
   }
 }

regression/cbmc/Pointer_array8/main.c

@@ -3249,6 +3249,24 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(infl_expr);
   }
+  else if(
+    identifier == CPROVER_PREFIX "round_to_integralf" ||
+    identifier == CPROVER_PREFIX "round_to_integrald" ||
+    identifier == CPROVER_PREFIX "round_to_integralld")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects two arguments" << eom;
+      throw 0;
+    }
+
+    auto round_to_integral_expr =
+      floatbv_round_to_integral_exprt{expr.arguments()[0], expr.arguments()[1]};
+    round_to_integral_expr.add_source_location() = source_location;
+
+    return std::move(round_to_integral_expr);
+  }
   else if(
     identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
     identifier == CPROVER_PREFIX "llabs" ||

regression/cbmc-library/__sort_of_CPROVER_round_to_integral-01/test.desc renamed to regression/cbmc/Pointer_array8/test.desc

@@ -94,6 +94,9 @@ int __CPROVER_islessgreaterf(float f, float g);
 int __CPROVER_islessgreaterd(double f, double g);
 int __CPROVER_isunorderedf(float f, float g);
 int __CPROVER_isunorderedd(double f, double g);
+float __CPROVER_round_to_integralf(float, int);
+double __CPROVER_round_to_integrald(double, int);
+long double __CPROVER_round_to_integralld(long double, int);
 
 // absolute value
 int __CPROVER_abs(int x);