ansi-c: clang extensions #2628

kroening · 2018-07-28T14:05:53Z

No description provided.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: aff0b39).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80288078
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: be6e3b6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80288229

smowton · 2018-07-30T09:37:47Z

Tests please

kroening · 2018-07-30T13:59:49Z

done

smowton · 2018-07-30T14:04:22Z

regression/ansi-c/gcc_float_types1/main.c

+int main()
+{
+  #ifndef __clang__
+  // on gcc, they can be re-declared, as they are identifiers, not keywords


Perhaps run the test against Clang too, but checking for the expected syntax error in the .desc file?

We don't have means to enable clang as preprocessor.

goto-cc --native-compiler=clang should do so, I believe?

Yes; are we willing to add clang as a dependency for CI for this?

I'd say it's more an "in principle we could" case. We'll probably do if/when we run into a regression on this :-)

tautschnig · 2018-07-30T14:15:21Z

src/util/config.cpp

-      defines.push_back("__BIG_ENDIAN__");
+#if defined(__APPLE__)
+    defines.push_back("__BIG_ENDIAN__");
+#endif


This looks wrong to me: it introduces a compile-time configuration into what ought to be a runtime configuration choice. This needs to test for the (target) operating system (os == "macos").

tautschnig · 2018-07-30T14:18:59Z

src/ansi-c/get-gcc-builtins.sh

@@ -102,7 +102,7 @@ cat > builtins.h <<EOF
 // some newer versions of GCC apparently support __floatXYZ
 #define dfloat32_type_node __float32
 #define dfloat64_type_node __float64
-#define dfloat128_type_node __float128
+#define dfloat128_type_node __CPROVER_Float128


Randomly placing this comment: the commit message says "bugfix" but it's not clear how this bug has been found/how a future regression is avoided?

This was found by running the existing regressions on FreeBSD, and repeating that should avoid it in the future as well.

tautschnig · 2018-07-30T14:19:51Z

src/ansi-c/scanner.l

@@ -1389,6 +1389,14 @@ __decltype          { if(PARSER.cpp98 &&
                return make_identifier();
            }

+  /* This is a clang extension */


Could a pointer to documentation be provided? Some day we may want to implement this.

tautschnig · 2018-07-30T14:20:59Z

src/ansi-c/ansi_c_internal_additions.cpp

-    // On 64-bit systems, both gcc and clang have typedefs
+    if(
+      config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
+      config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")


How has this subset of architectures been determined and/or why is it different from the __float128 one?

allredj

Passed Diffblue compatibility checks (cbmc commit: 3e11269).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80377005

allredj

Passed Diffblue compatibility checks (cbmc commit: f74c161).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80402711

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a

kroening added bugfix C Front End labels Jul 28, 2018

kroening assigned tautschnig and peterschrammel Jul 28, 2018

kroening requested review from tautschnig and peterschrammel July 28, 2018 14:05

kroening requested review from pkesseli and smowton as code owners July 28, 2018 14:05

kroening force-pushed the clang-extensions branch from d029ce8 to 2204f3a Compare July 28, 2018 14:27

kroening mentioned this pull request Jul 28, 2018

bugfix: __float80 is a typedef, not a keyword #2629

Closed

kroening force-pushed the clang-extensions branch 9 times, most recently from aff0b39 to be6e3b6 Compare July 28, 2018 16:25

allredj reviewed Jul 28, 2018

View reviewed changes

smowton reviewed Jul 30, 2018

View reviewed changes

tautschnig reviewed Jul 30, 2018

View reviewed changes

allredj reviewed Jul 30, 2018

View reviewed changes

kroening force-pushed the clang-extensions branch from 3e11269 to fb0878d Compare July 30, 2018 16:53

Daniel Kroening added 3 commits July 30, 2018 18:21

rename APPLE flavor to CLANG

3849bb0

bugfix: __float128

16a49a7

added _Null_unspecified clang extension

e63402e

Daniel Kroening added 3 commits July 30, 2018 18:21

FreeBSD: default flavor is now CLANG

5495625

__float80 is a typedef, not a keyword

8288a72

test for __float80 and __float128

f74c161

kroening force-pushed the clang-extensions branch from fb0878d to f74c161 Compare July 30, 2018 17:21

tautschnig approved these changes Jul 30, 2018

View reviewed changes

kroening merged commit 0618f7d into develop Jul 30, 2018

kroening deleted the clang-extensions branch July 30, 2018 18:00

allredj reviewed Jul 30, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ansi-c: clang extensions #2628

ansi-c: clang extensions #2628

kroening commented Jul 28, 2018

allredj left a comment

allredj left a comment

smowton commented Jul 30, 2018

kroening commented Jul 30, 2018

smowton Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

kroening Jul 30, 2018

tautschnig Jul 30, 2018

tautschnig Jul 30, 2018

allredj left a comment

allredj left a comment

ansi-c: clang extensions #2628

ansi-c: clang extensions #2628

Conversation

kroening commented Jul 28, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

smowton commented Jul 30, 2018

kroening commented Jul 30, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment