Problems with running CBMC with gcc from cygwin

[Daniel Ratiu]

Hello,

I am using Windows7, and a recent version of cygwin. I am trying to run: "cbmc --gcc -D__CYGWIN__ gcc_int32.c --function foo" on the following code:

---

#include <stdint.h>

void foo(int32_t x) {

assert(x > 0);

}

---

CBMC returns an error (below) due to the preprocessor. However, "gcc -E gcc_int32.c" works as expected.

Can you give me any hint?

Thank you!

With best regards,

Dan

--------------- CBMC error message:

CBMC version 5.6 64-bit x86_64 windows

Parsing gcc_int32.c

file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined

<built-in>: note: this is the location of the previous definition

In file included from /usr/include/stdint.h:13:0,

                 from /usr/lib/gcc/i686-pc-cygwin/5.4.0/include/stdint.h:9,

file                  from gcc_int32.c line 1:                  from gcc_int32.c:1:

file /usr/include/sys/_intsup.h line 89: /usr/include/sys/_intsup.h:89:2: error: #error "Unable to determine type definition of int32_t"

 #error "Unable to determine type definition of int32_t"

  ^

GCC preprocessing failed (fopen failed)

GCC preprocessing failed

PARSING ERROR

[Michael Tautschnig]

Hello Dan,

Apologies for top-posting, but I'd like to retain the full message below for
later discussion.

Would you be able to check whether running goto-cc works for you in this
setting? The way cbmc vs. goto-cc invoke the preprocessor differs a bit, and it
might help in debugging to see what those differences are. Presumably we are
missing some pre-defined macro, which will be one of `cpp -dM < /dev/null` -
could you possibly take a look at /usr/include/sys/_intsup.h to see what macros
it is testing for before reaching line 89?

Best,
Michael

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "CProver Support" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Daniel Ratiu]

Hello Michael,

thank you for the help!

I have tried goto-cl and I get the same error (attached is a screenshot with the error). 

As a workaround, I am using now the following command "cbmc --gcc -D_CYGWIN_ -D__INT32_TYPE__=int --function foo gcc_int32.c " -- now, cbmc works as expected.

In _intsup.h there is the following code (lines 84-90):

---

#if (__INT32_TYPE__ == 4 || __INT32_TYPE__ == 6)

#define _INT32_EQ_LONG

#elif __INT32_TYPE__ == 2

/* Nothing to define because int32_t is safe to print as an int. */

#else

#error "Unable to determine type definition of int32_t"

#endif

---

With best regards,

Dan

[Michael Tautschnig]

Hello Dan,

On Sun, Dec 11, 2016 at 4:07:26 -0800, 'Daniel Ratiu' via CProver Support wrote:
> Hello Michael,
>
> thank you for the help!
>
> I have tried goto-cl and I get the same error (attached is a screenshot
> with the error).
> As a workaround, I am using now the following command "cbmc --gcc
> -D_CYGWIN_ -D__INT32_TYPE__=int --function foo gcc_int32.c " -- now, cbmc
> works as expected.
>
> In _intsup.h there is the following code (lines 84-90):
> ---
> #if (__INT32_TYPE__ == 4 || __INT32_TYPE__ == 6)
> #define _INT32_EQ_LONG
> #elif __INT32_TYPE__ == 2
> /* Nothing to define because int32_t is safe to print as an int. */
> #else
> #error "Unable to determine type definition of int32_t"
> #endif
> ---
>

[...]

Would you be able to try out adding the __INT32_TYPE__ definition to
ansi-c/c_preprocess.cpp? As cpp -dM < /dev/null also has those, we may just need
to add them.

Best,
Michael

[Daniel Ratiu]

Hi Michael,

I have slightly modified c_preprocess as you suggested (I was not sure where to add the define, I hope that my place is meaningful) and now my CBMC works as expected. Attached is "git diff HEAD~1 c_preprocess.cpp"

Thank you!

With best regards,

Dan

--

---
You received this message because you are subscribed to a topic in the Google Groups "CProver Support" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/cprover-support/UpQag8DzF-w/unsubscribe.
To unsubscribe from this group and all its topics, send an email to cprover-support+unsubscribe@googlegroups.com.

[Michael Tautschnig]

Hi Dan,

On Sun, Dec 11, 2016 at 17:03:49 +0100, 'Daniel Ratiu' via CProver Support wrote:
> Hi Michael,
>
> I have slightly modified c_preprocess as you suggested (I was not sure
> where to add the define, I hope that my place is meaningful) and now my
> CBMC works as expected. Attached is "git diff HEAD~1 c_preprocess.cpp"
>

[...]

Many thanks for testing. I've pushed out

https://github.com/diffblue/cbmc/pull/348

to address this.

Best,
Michael