CBMCCodeGenerator.java 文件源码

private BooleanExpListNode generateAST(String code) {
    FormalPropertyDescriptionLexer l = new FormalPropertyDescriptionLexer(new ANTLRInputStream(code));
    CommonTokenStream ts = new CommonTokenStream(l);
    FormalPropertyDescriptionParser p = new FormalPropertyDescriptionParser(ts);

    BooleanExpScope declaredVars = new BooleanExpScope();

    preAndPostConditionsDescription.getSymbolicVariableList().forEach((v) -> {
        declaredVars.addTypeForId(v.getId(), v.getInternalTypeContainer());
    });

    return translator.generateFromSyntaxTree(
            p.booleanExpList(),
            electionDescription.getInputType().getType(),
            electionDescription.getOutputType().getType(),
            declaredVars);
}