Question about preprocess C project

[Andrew Valdez]

I am trying to use CPAchecker to verify a C language project, but I encountered issues when using the built-in preprocessing feature. I noticed in the documentation that the verification of multiple C files is still considered an experimental feature. Do I need to manually use gcc to preprocess the individual files in my C project?  

[Andrew Valdez]

I encountered an error while using --preprocess or preprocessing with gcc and then verifying the .i file with CPAchecker. The error message is: 

'Error: Parsing failed (/usr/lib/gcc/x86_64-linux-gnu/11/include/stdatomic.h, line 40: Syntax error: typedef _Atomic _Bool atomic_bool;) (EclipseCParser.buildCFA, SEVERE).' 

My C project can be compiled with gcc and run successfully, so I'm unsure how to resolve this issue. Anyway, after removing the relevant references, I can complete the preprocessing process.

But when I attempt to verify multiple files at once, such as using the command ‘../cpachecker/bin/cpachecker los_deadline.c los_process.c verifyCase.c --preprocess --64’, I encounter an exception:
'Exception in thread "main" com.google.common.base.VerifyException at com.google.common.base.Verify.verify(Verify.java:102) at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.AstLocationClassifier.visit(AstLocationClassifier.java:115) at org.eclipse.cdt.internal.core.dom.parser.c.CASTExpressionStatement.accept(CASTExpressionStatement.java:68) at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:89) at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:141) at org.eclipse.cdt.internal.core.dom.parser.ASTTranslationUnit.accept(ASTTranslationUnit.java:289) at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.AstCfaRelationBuilder.getASTCFARelation(AstCfaRelationBuilder.java:41) at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:348) at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseSomething(EclipseCParser.java:133) at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:152) at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseString(CParserWithLocationMapper.java:236) at org.sosy_lab.cpachecker.cfa.CParserWithPreprocessor.parseFiles(CParserWithPreprocessor.java:64) at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:721) at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:489) at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:432) at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:306) at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:171).'

I adjusted the files I verify each time; for example, in the first verification, I checked file A, and in the second verification, I checked files A and B, and so on for all 256 combinations of 8 files. Only 26 combinations can be verified, while the rest produce the above exception. I am confused about how to use this exception message to locate the problematic code or find the cause of the exception. If possible, I would greatly appreciate your advice.

[Andrew Valdez]

  Here are the C files I want to verify.  

On Tuesday, October 8, 2024 at 9:04:53 PM UTC+8 Andrew Valdez wrote:

[Philipp Wendler]

Dear Andrew,

thank you for your interest in CPAchecker!

Am 08.10.24 um 17:43 schrieb Andrew Valdez:

>
> I encountered an error while using --preprocess or preprocessing with gcc
> and then verifying the .i file with CPAchecker. The error message is:
>
> 'Error: Parsing failed
> (/usr/lib/gcc/x86_64-linux-gnu/11/include/stdatomic.h, line 40: Syntax
> error: typedef _Atomic _Bool atomic_bool;) (EclipseCParser.buildCFA,
> SEVERE).'

I am afraid that "_Atomic" is currently unsupported by CPAchecker.
If you do not need the atomic semantics, you could remove the "_Atomic"
keyword from the respective type definitions, or you just avoid
including stdatomic.h.
I created https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1253
to keep track of this, but I we currently do not have someone working on
this feature.

> But when I attempt to verify multiple files at once, such as using the
> command ‘../cpachecker/bin/cpachecker los_deadline.c los_process.c
> verifyCase.c --preprocess --64’, I encounter an exception:
> 'Exception in thread "main" com.google.common.base.VerifyException at
> com.google.common.base.Verify.verify(Verify.java:102) at
> org.sosy_lab.cpachecker.cfa.parser.eclipse.c.AstLocationClassifier.visit(AstLocationClassifier.java:115)

This is a bug that we would have to fix.
Unfortunately I cannot reproduce it with the files you sent because they
require header files that I do not have.
Could you please send me a combination of files that trigger this and
which are already preprocessed? Thanks!

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Andrew Valdez]

Thank you for your reply. Below is the preprocessed program.

[Philipp Wendler]

Dear Andrew,

sorry for the late reply, we were quite busy in the last few weeks
working on CPAchecker 4.0.

I can now reproduce your problem and even found some of our own files
triggering this.
I created an issue in our tracker for this:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1292
Feel free to subscribe for notifications to get updated on the status.
But I cannot make a promise on when this will be solved.
Thanks again for reporting this!

Greetings
Philipp

Am 12.10.24 um 05:10 schrieb Andrew Valdez: