Skip to content

Commit

Permalink
Changed Printer.print back to taking only a Program as input.
Browse files Browse the repository at this point in the history
The mode can be set via a setter now.
  • Loading branch information
ThomasHaas committed Jul 28, 2023
1 parent 8f65cc0 commit b7a22ef
Show file tree
Hide file tree
Showing 3 changed files with 20 additions and 37 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ private DebugPrint(String printHeader, Printer.Mode mode) {
@Override
public void run(Program program) {
System.out.println("======== " + printHeader + " ========");
System.out.println(new Printer().print(program, printerMode));
System.out.println(new Printer().setMode(printerMode).print(program));
System.out.println("======================================");
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -23,17 +23,14 @@ public enum Mode {

private boolean showAuxiliaryEvents = true;
private boolean showInitThreads = false;
private IDType idType = IDType.AUTO;
private Mode mode = Mode.ALL;

private final String paddingBase = " ";

public String print(Program program, Mode mode) {
public String print(Program program) {
result = new StringBuilder();
padding = new StringBuilder(paddingBase);

IDType origType = idType;
idType = resolveIDType(program);

String name = program.getName();
if(name == null){
name = "program";
Expand Down Expand Up @@ -65,22 +62,21 @@ public String print(Program program, Mode mode) {
}
}

idType = origType;
return result.toString();
}

public Printer setIdType(IDType type){
this.idType = type;
public Printer setShowAuxiliaryEvents(boolean flag) {
this.showAuxiliaryEvents = flag;
return this;
}

public Printer setShowAuxiliaryEvents(boolean flag){
this.showAuxiliaryEvents = flag;
public Printer setShowInitThreads(boolean flag) {
this.showInitThreads = flag;
return this;
}

public Printer setShowInitThreads(boolean flag){
this.showInitThreads = flag;
public Printer setMode(Mode mode) {
this.mode = mode;
return this;
}

Expand Down Expand Up @@ -115,7 +111,7 @@ private void appendEvent(Event event){
idSb.append(event.getGlobalId()).append(":");
result.append(idSb);
if(!(event instanceof Label)) {
result.append(" ");
result.append(" ");
}
result.append(padding, idSb.length(), padding.length());
result.append(event).append("\n");
Expand All @@ -125,17 +121,4 @@ private void appendEvent(Event event){
private boolean isAuxiliary(Event event){
return event instanceof Skip;
}

private IDType resolveIDType(Program program){
if(idType == IDType.AUTO){
if(program.isCompiled()) {
return IDType.COMPILED;
}
if(program.isUnrolled()){
return IDType.UNROLLED;
}
return IDType.ORIG;
}
return idType;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -21,60 +21,60 @@ public class PrinterTest {
@Test()
public void PrintBpl1() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "boogie/concurrency/fib_bench-1-O0.bpl"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
Compilation.newInstance().run(p);
LoopUnrolling.newInstance().run(p);
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
}

@Test()
public void PrintBpl2() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "locks/linuxrwlock.bpl"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
Compilation.newInstance().run(p);
LoopUnrolling.newInstance().run(p);
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
}

@Test()
public void PrintX86() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+mfence-rmw+rmw-mfence.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

@Test()
public void PrintPPC() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+lwsync+data-wsi-rfi-ctrlisync.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

@Test()
public void PrintAARCH64() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+popl+poap.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

@Test()
public void PrintLinux() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/C-rcu-link-after.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

@Test()
public void PrintLinux2() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.LITMUS_RESOURCE_PATH + "litmus/LKMM/dart/C-atomic-fetch-simple-01.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

@Test()
public void PrintLinux3() throws Exception {
Program p = new ProgramParser().parse(new File(ResourceHelper.LITMUS_RESOURCE_PATH + "litmus/LKMM/manual/atomic/C-atomic-01.litmus"));
assertNotNull(new Printer().print(p, Printer.Mode.ALL));
assertNotNull(new Printer().print(p));
assertNotNull(p.getSpecification().toString());
}

Expand Down

0 comments on commit b7a22ef

Please sign in to comment.