Possible bug: parse errors and workarounds for linux driver code
153 views
Skip to first unread message
objectiveK2
Jul 9, 2015, 8:56:27 AM7/9/15
to cpacheck...@googlegroups.com
Dear CPAChecker Community,
I'm trying to run CPAChecker against a linux driver, but I'm having parse errors.
I've identified which code is causing the parse error, then I've also found some workarounds.
Could you tell me if my workaround is appropriate, if there's other appropriate way, or if this is CPAChecker bug ?
Here is what I did:
1) preprocess the driver code
$ cd <kernel tree>
$ make drivers/net/ethernet/micrel/ks8851_mll.i
2) run cpa.sh
$ ./scripts/cpa.sh -predicateAnalysis ks8851_mll.i
3) observed error
"Error: Parsing failed (line **: Syntax error: _here: (unsigned long)&&_here;) (EclipseCParser.buildCFA, SEVERE)
The symptom occurs at a macro in "include/linux/kernel.h"
#define _THIS_IP_ ({ __label__ __here; __here: (unsigned long)&&__here; })
This means that a local label "__here" is declared, and returning its label address by '&&' operator.
Without an actual driver code, this can be easily reproduced by a simple C code like below.
#include <stdio.h>
int main(void) {
unsigned long foo = ({ __label__ __here; __here: (unsigned long)&&__here; });
printf("foo = %lu\n", foo);
return 0;
}
gcc compilation/preprocess will be succeeded against this simple code, but CPA checker fails with the same parse error message.
Then I've found two workaround for this:
1) Put parentheses around '$$__here'
If I change the expression like this, the symptom won't occur anymore, but another error message will appear.
- unsigned long hoge = ({ __label__ __here; __here: (unsigned long)&&__here; });
+ unsigned long hoge = ({ __label__ __here; __here: (unsigned long)(&&__here); });
Next error will be:
Error: Parsing failed(line **: Unsupported statement type CASTLabelStatement at end of compound-statement expression: _here: (unsigned long)(&&_here);) (EclipseCParser.buildCFA, SEVERE)
2) Put ; after label expression __here:
It seems CPAchecker accidentally tries to interpret : as a operator. So this error will disappear by the modification below.
- unsigned long hoge = ({ __label__ __here; __here: (unsigned long)(&&__here); });
+ unsigned long hoge = ({ __label__ __here; __here:; (unsigned long)(&&__here); });
This solves for the simple code.
But unfortunately for the actual driver code, next error is "java.lang.IllegalArgumentException" at Preconditions.checkAegument(Preconditions.java).
Are these workarounds valid? Is there known way to avoid this? Or Are they CPAChecker bug?
Also, is there any document/instruction/tutorial that would help me applying kernel driver source code for CPAChecker?
I've been looking for how svcomp benchmark verification tasks(Device Drivers Linux 64-bit) was generated, but I couldn't even preprocess any driver code with CIL tool.
Thank you very much in advance.
Kotaro Hashimoto
Hitachi Industry & Control Solutions, Ltd.
I'm trying to run CPAChecker against a linux driver, but I'm having parse errors.
I've identified which code is causing the parse error, then I've also found some workarounds.
Could you tell me if my workaround is appropriate, if there's other appropriate way, or if this is CPAChecker bug ?
Here is what I did:
1) preprocess the driver code
$ cd <kernel tree>
$ make drivers/net/ethernet/micrel/ks8851_mll.i
2) run cpa.sh
$ ./scripts/cpa.sh -predicateAnalysis ks8851_mll.i
3) observed error
"Error: Parsing failed (line **: Syntax error: _here: (unsigned long)&&_here;) (EclipseCParser.buildCFA, SEVERE)
The symptom occurs at a macro in "include/linux/kernel.h"
#define _THIS_IP_ ({ __label__ __here; __here: (unsigned long)&&__here; })
This means that a local label "__here" is declared, and returning its label address by '&&' operator.
Without an actual driver code, this can be easily reproduced by a simple C code like below.
#include <stdio.h>
int main(void) {
unsigned long foo = ({ __label__ __here; __here: (unsigned long)&&__here; });
printf("foo = %lu\n", foo);
return 0;
}
gcc compilation/preprocess will be succeeded against this simple code, but CPA checker fails with the same parse error message.
Then I've found two workaround for this:
1) Put parentheses around '$$__here'
If I change the expression like this, the symptom won't occur anymore, but another error message will appear.
- unsigned long hoge = ({ __label__ __here; __here: (unsigned long)&&__here; });
+ unsigned long hoge = ({ __label__ __here; __here: (unsigned long)(&&__here); });
Next error will be:
Error: Parsing failed(line **: Unsupported statement type CASTLabelStatement at end of compound-statement expression: _here: (unsigned long)(&&_here);) (EclipseCParser.buildCFA, SEVERE)
2) Put ; after label expression __here:
It seems CPAchecker accidentally tries to interpret : as a operator. So this error will disappear by the modification below.
- unsigned long hoge = ({ __label__ __here; __here: (unsigned long)(&&__here); });
+ unsigned long hoge = ({ __label__ __here; __here:; (unsigned long)(&&__here); });
This solves for the simple code.
But unfortunately for the actual driver code, next error is "java.lang.IllegalArgumentException" at Preconditions.checkAegument(Preconditions.java).
Are these workarounds valid? Is there known way to avoid this? Or Are they CPAChecker bug?
Also, is there any document/instruction/tutorial that would help me applying kernel driver source code for CPAChecker?
I've been looking for how svcomp benchmark verification tasks(Device Drivers Linux 64-bit) was generated, but I couldn't even preprocess any driver code with CIL tool.
Thank you very much in advance.
Kotaro Hashimoto
Hitachi Industry & Control Solutions, Ltd.
Vadim Mutilin
Jul 9, 2015, 9:23:58 AM7/9/15
to cpacheck...@googlegroups.com, hasimot...@gmail.com
Hi Kotaro!
This is a known bug in Eclipse CDT which is used inside CPAchecker
https://bugs.eclipse.org/bugs/show_bug.cgi?id=84144#c13
For compiling Linux kernel we are using workaround
To generate verifications tasks for Linux kernel you can use LDV Tools (http://forge.ispras.ru/projects/ldv).
If you want to use prebuilt LDV Tools, please follow our LDV Tools in Docker instructions.
To run CPAchecker use environment variable RCV_VERIFIER=cpachecker
Best,
Vadim
09.07.2015 15:56, objectiveK2 пишет:
This is a known bug in Eclipse CDT which is used inside CPAchecker
https://bugs.eclipse.org/bugs/show_bug.cgi?id=84144#c13
For compiling Linux kernel we are using workaround
sed -i -e 's/#define _THIS_IP_ .*/#define _THIS_IP_ ({0;})/' include/linux/kernel.h;
To generate verifications tasks for Linux kernel you can use LDV Tools (http://forge.ispras.ru/projects/ldv).
If you want to use prebuilt LDV Tools, please follow our LDV Tools in Docker instructions.
To run CPAchecker use environment variable RCV_VERIFIER=cpachecker
Best,
Vadim
09.07.2015 15:56, objectiveK2 пишет:
--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Philipp Wendler
Jul 9, 2015, 12:06:26 PM7/9/15
to cpacheck...@googlegroups.com
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Dear Kotaro,
Am 09.07.2015 um 14:56 schrieb objectiveK2:
> I'm trying to run CPAChecker against a linux driver, but I'm having
> parse errors. I've identified which code is causing the parse
> error, then I've also found some workarounds. Could you tell me if
> my workaround is appropriate, if there's other appropriate way, or
> if this is CPAChecker bug ?
>
> Here is what I did: 1) preprocess the driver code $ cd <kernel
> tree> $ make drivers/net/ethernet/micrel/ks8851_mll.i
>
> 2) run cpa.sh $ ./scripts/cpa.sh -predicateAnalysis ks8851_mll.i
>
> 3) observed error "Error: Parsing failed (line **: Syntax error:
> _here: (unsigned long)&&_here;) (EclipseCParser.buildCFA, SEVERE)
>
>
> The symptom occurs at a macro in "include/linux/kernel.h"
>
> #define _THIS_IP_ ({ __label__ __here; __here: (unsigned
> long)&&__here; })
As Vadim already wrote, this is a bug in Eclipse CDT.
We have reported it and they have fixed it already,
so we are currently just waiting for a released version of CDT
that includes the change.
In practice, most occurrences of this macro are not relevant for
verification purposes as they only serve to produce a unique id,
thus I recommend to use the redefinition of the macro as a workaround
like Vadim proposed.
You can also maybe also use a preprocessor argument to overwrite the
macro definition without actually changing the file.
> Then I've found two workaround for this:
>
> 1) Put parentheses around '$$__here' If I change the expression
> like this, the symptom won't occur anymore, but another error
> message will appear. - unsigned long hoge = ({ __label__ __here;
> __here: (unsigned long)&&__here; }); + unsigned long hoge = ({
> __label__ __here; __here: (unsigned long)(&&__here); });
>
> Next error will be: Error: Parsing failed(line **: Unsupported
> statement type CASTLabelStatement at end of compound-statement
> expression: _here: (unsigned long)(&&_here);)
> (EclipseCParser.buildCFA, SEVERE)
This should work, but it seems the AST inside this ({ }) expression
is too complex for CPAchecker here. I will look into this.
> 2) Put ; after label expression __here: It seems CPAchecker
> accidentally tries to interpret : as a operator. So this error will
> disappear by the modification below. - unsigned long hoge = ({
> __label__ __here; __here: (unsigned long)(&&__here); }); +
> unsigned long hoge = ({ __label__ __here; __here:; (unsigned
> long)(&&__here); });
>
> This solves for the simple code. But unfortunately for the actual
> driver code, next error is "java.lang.IllegalArgumentException" at
> Preconditions.checkAegument(Preconditions.java).
Could you please post the full stack trace for this error?
Preconditions is just a helper method that is called in a lot of places.
> Also, is there any document/instruction/tutorial that would help me
> applying kernel driver source code for CPAChecker? I've been
> looking for how svcomp benchmark verification tasks(Device Drivers
> Linux 64-bit) was generated, but I couldn't even preprocess any
> driver code with CIL tool.
The best solution I know would be to use the LDV tools as recommended
by Vadim.
Greetings, Philipp
- --
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1
iQIcBAEBAgAGBQJVnpv/AAoJEGLA94wxqd6M8msQAI/bspMPOlKvf5iAaLytdVck
3e7ul4exYVfFb2+wt0rEREbaLiq3KKLn24v/+QNoUMb81NEI5u/vzBkjxDm9MvxR
Xe+wy4Mn5yTG/ORRMCi+Mt1reP0VynNfzF/V1NhZlbm9tQ3K5CJz2jgVv3mBykQh
53PMTznkD73ziqKGVQwXpbeNTG/A6fZG6vv5C1vvFVb3naiQqWfiXMCcv5+b7W39
swIJM0p0W1+Qj47cFWnDpTBi6Ha/dIa70a0jYsne4+9nmGQ4UHYY/kyMSPVXAWOJ
K/PhBpOHA3CQQ9uaSoHXG/W9U/l5iUEhtWO1dv6FOy2OwezOEHaC2S/h+Ve+gl3+
mZDm4YqJt9a0DD0whG5817wmMYnjZNNRuxqFziIjI0gMp8n+R3FvSVGxAvbmPmxU
w062JhHGx1fnbbNJn8XmPeo3+bPJtOIO5NZr+iQuOsjMKmDsbpo01acxJsUQn2XE
nbVKFOlz8CVEhy01SVH25Eg7idI34G9W55pvrrFlBQzFKYYlKJ6KY3Yrfh3BalTe
aDSK176YO1Qdm+2Bt8/FjkrTEAWM/jUCxIETERLdtegiyZSnE8/wOKizI1IGnJ7N
EldXdGcVFfXLNXqyrOFjHcnCJFNoRZ5R9MkpglE5bDDkM/i8fZLQkjq2nnUJ8F2U
Zj6Tioms7FEdv0h29JI5
=GH52
-----END PGP SIGNATURE-----
Hash: SHA1
Dear Kotaro,
Am 09.07.2015 um 14:56 schrieb objectiveK2:
> I'm trying to run CPAChecker against a linux driver, but I'm having
> parse errors. I've identified which code is causing the parse
> error, then I've also found some workarounds. Could you tell me if
> my workaround is appropriate, if there's other appropriate way, or
> if this is CPAChecker bug ?
>
> Here is what I did: 1) preprocess the driver code $ cd <kernel
> tree> $ make drivers/net/ethernet/micrel/ks8851_mll.i
>
> 2) run cpa.sh $ ./scripts/cpa.sh -predicateAnalysis ks8851_mll.i
>
> 3) observed error "Error: Parsing failed (line **: Syntax error:
> _here: (unsigned long)&&_here;) (EclipseCParser.buildCFA, SEVERE)
>
>
> The symptom occurs at a macro in "include/linux/kernel.h"
>
> #define _THIS_IP_ ({ __label__ __here; __here: (unsigned
> long)&&__here; })
We have reported it and they have fixed it already,
so we are currently just waiting for a released version of CDT
that includes the change.
In practice, most occurrences of this macro are not relevant for
verification purposes as they only serve to produce a unique id,
thus I recommend to use the redefinition of the macro as a workaround
like Vadim proposed.
You can also maybe also use a preprocessor argument to overwrite the
macro definition without actually changing the file.
> Then I've found two workaround for this:
>
> 1) Put parentheses around '$$__here' If I change the expression
> like this, the symptom won't occur anymore, but another error
> message will appear. - unsigned long hoge = ({ __label__ __here;
> __here: (unsigned long)&&__here; }); + unsigned long hoge = ({
> __label__ __here; __here: (unsigned long)(&&__here); });
>
> Next error will be: Error: Parsing failed(line **: Unsupported
> statement type CASTLabelStatement at end of compound-statement
> expression: _here: (unsigned long)(&&_here);)
> (EclipseCParser.buildCFA, SEVERE)
is too complex for CPAchecker here. I will look into this.
> 2) Put ; after label expression __here: It seems CPAchecker
> accidentally tries to interpret : as a operator. So this error will
> disappear by the modification below. - unsigned long hoge = ({
> __label__ __here; __here: (unsigned long)(&&__here); }); +
> unsigned long hoge = ({ __label__ __here; __here:; (unsigned
> long)(&&__here); });
>
> This solves for the simple code. But unfortunately for the actual
> driver code, next error is "java.lang.IllegalArgumentException" at
> Preconditions.checkAegument(Preconditions.java).
Preconditions is just a helper method that is called in a lot of places.
> Also, is there any document/instruction/tutorial that would help me
> applying kernel driver source code for CPAChecker? I've been
> looking for how svcomp benchmark verification tasks(Device Drivers
> Linux 64-bit) was generated, but I couldn't even preprocess any
> driver code with CIL tool.
by Vadim.
Greetings, Philipp
- --
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1
iQIcBAEBAgAGBQJVnpv/AAoJEGLA94wxqd6M8msQAI/bspMPOlKvf5iAaLytdVck
3e7ul4exYVfFb2+wt0rEREbaLiq3KKLn24v/+QNoUMb81NEI5u/vzBkjxDm9MvxR
Xe+wy4Mn5yTG/ORRMCi+Mt1reP0VynNfzF/V1NhZlbm9tQ3K5CJz2jgVv3mBykQh
53PMTznkD73ziqKGVQwXpbeNTG/A6fZG6vv5C1vvFVb3naiQqWfiXMCcv5+b7W39
swIJM0p0W1+Qj47cFWnDpTBi6Ha/dIa70a0jYsne4+9nmGQ4UHYY/kyMSPVXAWOJ
K/PhBpOHA3CQQ9uaSoHXG/W9U/l5iUEhtWO1dv6FOy2OwezOEHaC2S/h+Ve+gl3+
mZDm4YqJt9a0DD0whG5817wmMYnjZNNRuxqFziIjI0gMp8n+R3FvSVGxAvbmPmxU
w062JhHGx1fnbbNJn8XmPeo3+bPJtOIO5NZr+iQuOsjMKmDsbpo01acxJsUQn2XE
nbVKFOlz8CVEhy01SVH25Eg7idI34G9W55pvrrFlBQzFKYYlKJ6KY3Yrfh3BalTe
aDSK176YO1Qdm+2Bt8/FjkrTEAWM/jUCxIETERLdtegiyZSnE8/wOKizI1IGnJ7N
EldXdGcVFfXLNXqyrOFjHcnCJFNoRZ5R9MkpglE5bDDkM/i8fZLQkjq2nnUJ8F2U
Zj6Tioms7FEdv0h29JI5
=GH52
-----END PGP SIGNATURE-----
objectiveK2
Jul 9, 2015, 10:21:17 PM7/9/15
to cpacheck...@googlegroups.com
Dear Vadim, Greetings,
Thank you very much for your kind support.
Thank you very much for your kind support.
> The best solution I know would be to use the LDV tools as recommended by Vadim.
Yes, I'll try to use LDV tools for driver verification.
> Could you please post the full stack trace for this error?
> Preconditions is just a helper method that is called in a lot of places.
Below is the error stack trace with the workaround(redefining the macro _THIS_IP_ with {0;}) and the following operations:
$ make drivers/net/ethernet/micrel/ks8851_mll.i
line 19289: Dead code detected: [!(erratum_a15_798181_handler == 0)] (CFACreationUtils.addEdgeToCFA, INFO)
line 19579: Dead code detected: return 1; (CFACreationUtils.addEdgeToCFA, INFO)
line 19584: Dead code detected: return 0; (CFACreationUtils.addEdgeToCFA, INFO)
Exception in thread "main" java.lang.IllegalArgumentException
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:108)
at org.sosy_lab.cpachecker.cfa.ast.c.CVariableDeclaration.<init>(CVariableDeclaration.java:57)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.createDeclaration(ASTConverter.java:1609)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1520)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.createEdgeForDeclaration(CFAFunctionBuilder.java:328)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.handleSimpleDeclaration(CFAFunctionBuilder.java:307)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.visit(CFAFunctionBuilder.java:276)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTSimpleDeclaration.accept(CASTSimpleDeclaration.java:91)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTDeclarationStatement.accept(CASTDeclarationStatement.java:77)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:81)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:133)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.handleFunctionDefinition(CFABuilder.java:361)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.createCFA(CFABuilder.java:316)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:339)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:181)
at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseFile(CParserWithLocationMapper.java:102)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:540)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:360)
at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:361)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:246)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:133)
----------------
Exactly the same exception occurs for other driver codes, as far as I tried "drivers/net/wireless/ath/ath6kl/usb.i" and "drivers/net/phy/micrel.i" in kernel 3.19.5.
Thank you.
Kotaro Hashimoto
2015年7月10日金曜日 1時06分26秒 UTC+9 Philipp Wendler:
$ make drivers/net/ethernet/micrel/ks8851_mll.i
$ ./scripts/cpa.sh -predicateAnalysis ks8851_mll.i
----------------line 19289: Dead code detected: [!(erratum_a15_798181_handler == 0)] (CFACreationUtils.addEdgeToCFA, INFO)
line 19579: Dead code detected: return 1; (CFACreationUtils.addEdgeToCFA, INFO)
line 19584: Dead code detected: return 0; (CFACreationUtils.addEdgeToCFA, INFO)
Exception in thread "main" java.lang.IllegalArgumentException
at com.google.common.base.Preconditions.checkArgument(Preconditions.java:108)
at org.sosy_lab.cpachecker.cfa.ast.c.CVariableDeclaration.<init>(CVariableDeclaration.java:57)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.createDeclaration(ASTConverter.java:1609)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1520)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.createEdgeForDeclaration(CFAFunctionBuilder.java:328)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.handleSimpleDeclaration(CFAFunctionBuilder.java:307)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.visit(CFAFunctionBuilder.java:276)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTSimpleDeclaration.accept(CASTSimpleDeclaration.java:91)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTDeclarationStatement.accept(CASTDeclarationStatement.java:77)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:81)
at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:133)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.handleFunctionDefinition(CFABuilder.java:361)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.createCFA(CFABuilder.java:316)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:339)
at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:181)
at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseFile(CParserWithLocationMapper.java:102)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:540)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:360)
at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:361)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:246)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:133)
----------------
Exactly the same exception occurs for other driver codes, as far as I tried "drivers/net/wireless/ath/ath6kl/usb.i" and "drivers/net/phy/micrel.i" in kernel 3.19.5.
Thank you.
Kotaro Hashimoto
2015年7月10日金曜日 1時06分26秒 UTC+9 Philipp Wendler:
Philipp Wendler
Jul 13, 2015, 4:08:14 AM7/13/15
to cpacheck...@googlegroups.com
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Dear Kotaro,
Hash: SHA1
Dear Kotaro,
Am 10.07.2015 um 04:21 schrieb objectiveK2:
>> Could you please post the full stack trace for this error?
>> Preconditions is just a helper method that is called in a lot of
>> places.
>
> Below is the error stack trace with the workaround(redefining the
> macro _THIS_IP_ with {0;}) and the following operations: $ make
> drivers/net/ethernet/micrel/ks8851_mll.i $ ./scripts/cpa.sh
> -predicateAnalysis ks8851_mll.i
Sorry, I am a little bit confused now.
>> Could you please post the full stack trace for this error?
>> Preconditions is just a helper method that is called in a lot of
>> places.
>
> Below is the error stack trace with the workaround(redefining the
> macro _THIS_IP_ with {0;}) and the following operations: $ make
> drivers/net/ethernet/micrel/ks8851_mll.i $ ./scripts/cpa.sh
> -predicateAnalysis ks8851_mll.i
Is this error appearing as you wrote with your original workaround of
inserting ";" into the macro, or with Vadims workaround of redeclaring
it as ({0;}), or with both?
Also, could you please send me a file with which this is happening?
I tried following your steps, but could not reproduce it
as CPAchecker reports some syntax error about assembler code instead.
Greetings, Philipp
- --
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093
-----BEGIN PGP SIGNATURE-----
iQIcBAEBAgAGBQJVo3HrAAoJEGLA94wxqd6MWfkP+waAbUWMrd9o0ZZLLcM70+2C
KvQvFaYUZkKb8dZx8Z/3FppFxJXzshEChfoYIlwAHTL4LYM0XgKmTNHXsVUs45P6
wDv+yIpLi6Y55q+Nhwu2c42OFcoD066w/xTpYl754ckn2m58otv5LJ2P9LoD0nDI
Dj9YT4cRhhruFhjHSQNr9xK2rU8gauBQM2ZlopujPP9c/ZJ/fUqOmCRcV2v6tnhK
vgW4Q/THVq/5boat3xuX/KIXQVxvQPEGYjORg+pGUZZxcg0tJsqhxO+V3G7qdNnP
/bhosGBrlf9c92f9qA3Va8Ler3B1Bobt6vJV716HpP4t1Hrdlpm9DCYKImFVlqnt
UJFI2PWHQ3SGWzCiHnPQ3xhUeQ7Lm5gf1HorG5HGySiPQ6wihOfgh3cUKuN/Brwc
Te5/6Lc1HkuRCR3LjpDpDZSWhlmRtped7Ge006Ni8CsIkCZc1uD9r+TkGlPX4C6w
PcmNhpl8TbFG6r6Mtm8ZJ+g+lnOihxgSuuZDFsmf2DZW0U1tc/VP3qilMhVznzGs
v44F7mUmDkOuz6v7Qb6DLrYPfFqkiJEoWvhU5bLZKqixWRc6QQxwsKGD5kK6fDa+
RP3dDi4/l0RRvtVFqM7Yw05LYiNHx+/ijIZ7/xkZG4GBajfJwbxXd62d4KadmLON
qUtIKRpE7XAsAJohddRX
=5lE7
-----END PGP SIGNATURE-----
objectiveK2
Jul 13, 2015, 4:43:21 AM7/13/15
to cpacheck...@googlegroups.com
Dear Phillipp,
Thank you for your investigation.
Thank you for your investigation.
> Is this error appearing as you wrote with your original workaround of
> inserting ";" into the macro, or with Vadims workaround of redeclaring
> it as ({0;}), or with both?
I tried both, and the results were the same.
> Also, could you please send me a file with which this is happening?
Please find the attached file "ks8851_mll.i".
> I tried following your steps, but could not reproduce it
> as CPAchecker reports some syntax error about assembler code instead.
Sorry for the confusion, the step I wrote($ make drivers/net/ethernet/micrel/ks8851_mll.i)
was cross compilation via Yocto Project(BitBake recipe), not directly from the terminal.
If I hit it from the host with native gcc, I'm also getting a syntax error below.
Error: Parsing failed (line 1354: Syntax error: asm goto("1: jmp %l[t_no]\n" "2:\n" ".section .altinstructions,\"a\"\n" " .long 1b - .\n" " .long 0\n" " .word %P0\n" " .byte 2b - 1b\n" " .byte 0\n" ".previous\n" : : "i" (bit) : : t_no);) (EclipseCParser.buildCFA, SEVERE)
> The best solution I know would be to use the LDV tools.
I'm successfully working on LDV Tools in Docker right now. Thank you very much for the info.
Best regards,
Kotaro Hashimoto
2015年7月13日月曜日 17時08分14秒 UTC+9 Philipp Wendler:
was cross compilation via Yocto Project(BitBake recipe), not directly from the terminal.
If I hit it from the host with native gcc, I'm also getting a syntax error below.
Error: Parsing failed (line 1354: Syntax error: asm goto("1: jmp %l[t_no]\n" "2:\n" ".section .altinstructions,\"a\"\n" " .long 1b - .\n" " .long 0\n" " .word %P0\n" " .byte 2b - 1b\n" " .byte 0\n" ".previous\n" : : "i" (bit) : : t_no);) (EclipseCParser.buildCFA, SEVERE)
> The best solution I know would be to use the LDV tools.
I'm successfully working on LDV Tools in Docker right now. Thank you very much for the info.
Best regards,
Kotaro Hashimoto
2015年7月13日月曜日 17時08分14秒 UTC+9 Philipp Wendler:
Philipp Wendler
Jul 13, 2015, 6:16:27 AM7/13/15
to cpacheck...@googlegroups.com
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Dear Kotaro,
Hash: SHA1
Dear Kotaro,
Am 13.07.2015 um 10:43 schrieb objectiveK2:
>> Is this error appearing as you wrote with your original
>> workaround of inserting ";" into the macro, or with Vadims
>> workaround of redeclaring it as ({0;}), or with both?
> I tried both, and the results were the same.
>
>
>> Also, could you please send me a file with which this is
>> happening?
> Please find the attached file "ks8851_mll.i".
Thanks, I can reproduce it now.
>> Is this error appearing as you wrote with your original
>> workaround of inserting ";" into the macro, or with Vadims
>> workaround of redeclaring it as ({0;}), or with both?
> I tried both, and the results were the same.
>
>
>> Also, could you please send me a file with which this is
>> happening?
> Please find the attached file "ks8851_mll.i".
It is actually an unrelated feature that is missing here
(local variables declared as extern),
but as it seems to be working for you now,
I just added a better error message.
Greetings, Philipp
- --
Philipp Wendler
Lehrstuhl für Softwaresysteme
Universität Passau
Raum IM 110 - Tel.: 0851/509-3093
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)
uXuB6Gvc+BN9POMyEs+1so2fosekjfoETlMh/o2g1z+l7HfAUhgafttMRXdEcArU
NwKU1dmRc73yzevhiJJOyraMrRlD8ahRjApaSl2dgOk1gaJoFXMOeJ7Y9NSsfzoU
IzlzWVSbqFIZgGrojkjkkE4eomURH+yG1pmi4+IpP916ju33Hrf8JSd0/dMuDmw3
UIz7lkghJcoxAEXfnfJBReXO7cimX/8L3BhFdV/N7H39SERO7/pMbSq9pO/CUpus
Df//a11L70zZeoa5/HreO3/Ak5gzCbHoI/9D+t1ErqM8iw+4rYKbSWhUMErICL2f
h0S188YZ6RqYIHQA7Q3/CF/xh1JIQyQx2gBPsydpanil0MPOMZ/Ss22b2PLt+R/z
4RoqGeEG4jy+JM5w6Tutj3kx3pcLkcGk/TPYlGxsMsMXCbi7fuDAf0LXV50/Hg5i
JszNKv5m+0bbt6NxlEAIXDlT22JOwtggMq7EmiAG0I9jCXQg4EFgd1yLZ80JbMCt
iQk5Hhujiw+UwFseLJm9tELkipUsWlRB86dnX62V0F4HBt1EPJ/3UeKbJ7AQ9YTw
nXUueQXPQ9BTq2aOVCYymMjJusnDbbWh0PRfF3WeI1OipCLEltha2bbGi+JnbDBX
DSvL8GdjTwYsqsu7VYd8
=lV1P
-----END PGP SIGNATURE-----
Reply all
Reply to author
Forward
0 new messages