INNER CODE UNIT · Python

expected_output

MPC-SoK/frameworks · cbmc-gc/source/geninput.py:60

    expected_output = [0] * BINS
    for idA in range(LEN):
        for idB in range(LEN):
            if arA[ID][idA] == arB[ID][idB]:
                expected_output[ arB[VAL][idB] ] += arA[VAL][idA]
    
    # write values 
    for player,ar in [("A",arA),("B",arB)]:
        pl = str_iv(player, str_struct(["d"],[ar]))
        fo.write(pl)

    output = str_struct(["d"], [[eo % 256 for eo in expected_output]])
    fo.write("return_value == %s;\n"%(output))

if __name__ == "__main__":
    parser = argparse.ArgumentParser(
        description='generates input for cbmc-gc sample programs')
    #parser.add_argument('-l', default=10, type=int, 

View source record →