Bug #5404: [verilog][parser][cfg] java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN - Retrascope - Open-Source Projects

Actions

Copy link

Bug #5404

closed

[verilog][parser][cfg] java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN

Added by Sergey Smolov over 9 years ago. Updated over 9 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Alexander Kamkin

Category:

Target version:

0.1

Start date:

11/02/2014

Due date:

% Done:

Estimated time:

Detected in build:

svn

Platform:

Published in build:

r1324

Description

Running: verilog-parser
Options: {v=[D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v], args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer}
2014.11.02 14:02:28.860. INFO: Start observing module ram.
2014.11.02 14:02:28.860. INFO: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.861. INFO: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.862. INFO: add variable val_rd [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.862. INFO: add variable val_wr [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.863. INFO: add variable addr_in [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.11.02 14:02:28.864. INFO: add variable data_in [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.864. INFO: add variable val_out [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.865. INFO: add variable data_out [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.866. INFO: add variable is_ready [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.866. INFO: add variable mem0 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.867. INFO: add variable mem1 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.868. INFO: add variable mem2 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.868. INFO: add variable mem3 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.869. INFO: add variable result [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.870. INFO: add variable state [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.11.02 14:02:28.871. INFO: add variable RAM_IDLE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.875. INFO: add variable RAM_READ [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.876. INFO: add variable RAM_WRITE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.877. INFO: add variable RAM_RESULT [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
Storing: cfg

Running: cfg-cgaa-transformer
Options: {args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer, cfg=<cfg>}
Storing: cgaa

Running: cgaa-efsm-transformer
Options: {cgaa=<cgaa>, args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer}
2014.11.02 14:02:28.888. ERROR: The exception has been encountered: java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:147)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:303)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:282)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:209)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:152)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:127)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:100)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:120)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:350)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:335)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:203)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:192)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:183)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:255)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:133)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:247)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:229)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:247)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:229)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:213)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:204)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:195)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:179)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:166)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:86)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:126)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:191)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:191)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:117)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:320)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:341)
at ru.ispras.retrascope.util.VerilogUtilTest.runRetrascope(VerilogUtilTest.java:120)
at ru.ispras.retrascope.util.VerilogUtilTest.runVerilog(VerilogUtilTest.java:69)
at ru.ispras.retrascope.util.HdlUtilTest.runVerilog(HdlUtilTest.java:137)
at ru.ispras.retrascope.util.HdlUtilTest.runHdl(HdlUtilTest.java:51)

Actions

Copy link

Updated by Sergey Smolov over 9 years ago

Воспроизвести ошибку можно путем запуска Retrascope с указанными параметрами.

В некоторых jUnit-тестах сейчас обработка Verilog-описаний отключена, т.к. приводит к падению, а именно в:

ru/ispras/retrascope/engine/cgaa/printer/graphml/CgaaGraphMlPrinterTestCase
ru/ispras/retrascope/engine/efsm/printer/graphml/EfsmGraphMlPrinterModuleTestCase

См. также TODO в ru/ispras/retrascope/util/HdlUtilTest.java

Actions

Copy link

Updated by Mikhail Chupilko over 9 years ago

Assignee changed from Mikhail Chupilko to Alexander Kamkin

Добавил отладочный вывод в случае UNKNOWN-типов у выражений. Выяснилось, что данные проблемы порождаются by Nodes with numeric constants (Literals, which Fortress doesn't know, and not going to know). What should I do having an access to nothing of Node but elaborated type "UNKNOWN" (by getDataType())?

2014.12.11 18:55:21.159. INFO: Retrascope is starting
Running: verilog-parser
Options: {args=src/test/verilog/ram/ram.v --target efsm, v=[src/test/verilog/ram/ram.v]}
Including file 'src/test/verilog/ram/ram.v'
2014.12.11 18:55:21.406. INFO: Start observing module ram.
2014.12.11 18:55:21.407. INFO: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.407. INFO: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable val_rd [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable val_wr [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable addr_in [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable data_in [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.409. INFO: add variable val_out [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.411. INFO: add variable data_out [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable is_ready [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem0 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem1 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem2 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem3 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.413. INFO: add variable result [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.413. INFO: add variable state [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.12.11 18:55:21.417. INFO: add variable RAM_IDLE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_IDLE is UNKNOWN
[parseAssignment2] DataType of 2'h0 is UNKNOWN
2014.12.11 18:55:21.422. INFO: add variable RAM_READ [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_READ is UNKNOWN
[parseAssignment2] DataType of 2'h1 is UNKNOWN
2014.12.11 18:55:21.422. INFO: add variable RAM_WRITE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_WRITE is UNKNOWN
[parseAssignment2] DataType of 2'h2 is UNKNOWN
2014.12.11 18:55:21.423. INFO: add variable RAM_RESULT [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_RESULT is UNKNOWN
[parseAssignment2] DataType of 2'h3 is UNKNOWN
[parseAssignment] DataType of is_ready is UNKNOWN
[parseAssignment] DataType of val_out is UNKNOWN
[parseAssignment] DataType of data_out is UNKNOWN
[parseAssignment] DataType of mem0 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem1 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem2 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem3 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 2'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h1 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h2 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem0 is UNKNOWN
[parseAssignment] DataType of mem1 is UNKNOWN
[parseAssignment] DataType of mem2 is UNKNOWN
[parseAssignment] DataType of mem3 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h3 is UNKNOWN
Storing: cfg

Running: cfg-cgaa-transformer
Options: {args=src/test/verilog/ram/ram.v --target efsm, cfg=<cfg>}
Storing: cgaa

Running: cgaa-efsm-transformer
Options: {args=src/test/verilog/ram/ram.v --target efsm, cgaa=<cgaa>}
2014.12.11 18:55:21.562. ERROR: The exception has been encountered: java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:146)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:378)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:356)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:204)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:142)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:117)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:89)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:110)
at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:307)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:206)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:199)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:188)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:261)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:219)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:157)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:210)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:201)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:185)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:172)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:92)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:133)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:115)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:325)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:346)

2014.12.11 18:55:21.564. INFO: Retrascope is shutting down
Exception in thread "main" java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:146)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:378)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:356)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:204)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:142)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:117)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:89)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:110)
at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:307)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:206)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:199)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:188)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:261)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:219)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:157)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:210)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:201)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:185)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:172)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:92)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:133)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:115)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:325)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:346)