locked
Pex From Code (Z3, Dynamic Symbolic Execution) RRS feed

  • Question

  • I have a simple method, for example:

    public int MyMethod(int a){
                if (a == 0)
                    return 1;

                else
                    return 2;
    }

    Is there a class in Microsoft.Pex.Framework.dll which will solve the path conditions for me if I pass this method to it?

    I am trying to use Microsoft's bit of handy work so that I do not have to go to Z3 directly.

    Thank you.

    Friday, November 10, 2017 3:10 AM

Answers

  • >>Is there a class in Microsoft.Pex.Framework.dll which will solve the path conditions for me if I pass this method to it?

    I'm afraid not, according to the IntelliTest official doc. which does not mention any class that could make it.

    As Jack had suggested, you could post a thread on stack overflow where the PEX team there might give you some other advice.

    Your understanding and cooperation will be grateful.

    Have a good day:)

     

    Regards,

    Fletcher


    MSDN Community Support
    Please remember to click "Mark as Answer" the responses that resolved your issue, and to click "Unmark as Answer" if not. This can be beneficial to other community members reading this thread. If you have any compliments or complaints to MSDN Support, feel free to contact MSDNFSF@microsoft.com.



    Monday, November 27, 2017 8:18 AM

All replies

  • I am trying to find the paths for variable a in the above method.
    Friday, November 10, 2017 3:12 AM
  • I do also have the method 'MyMethod' in a syntax tree. I can place it in any other data structure but I thought there might be a simple conversion for a syntax tree to Z3 notation.
    Friday, November 10, 2017 3:37 AM
  • Hi Stumple,

    Thanks for your posting.

    Just found a thread with similar issue, the answer from pvlakshm explained it specifically, please have a look, and let me know if it could resolve your issue:

    https://stackoverflow.com/questions/41336152/pex-how-to-obtain-all-path-conditions-pc

    Have a nice day:)

     

    Best regards,

    Fletcher  


    MSDN Community Support
    Please remember to click "Mark as Answer" the responses that resolved your issue, and to click "Unmark as Answer" if not. This can be beneficial to other community members reading this thread. If you have any compliments or complaints to MSDN Support, feel free to contact MSDNFSF@microsoft.com.


    • Edited by Fletch Zhou Monday, November 13, 2017 8:54 AM
    • Proposed as answer by Fletch Zhou Wednesday, November 15, 2017 9:44 AM
    Monday, November 13, 2017 8:54 AM
  • Hi Stumple,

    The Pex team indicating that based on community feedback they are now lurking in the stack forums

    http://stackoverflow.com/questions/tagged/pex

    So if possible, you could post your issue in the pex support site, and there you would get dedicated support.

    Best Regards,

    Jack


    MSDN Community Support
    Please remember to click "Mark as Answer" the responses that resolved your issue, and to click "Unmark as Answer" if not. This can be beneficial to other community members reading this thread. If you have any compliments or complaints to MSDN Support, feel free to contact MSDNFSF@microsoft.com.

    Thursday, November 23, 2017 5:21 AM
  • I want to make the call to Intellitest myself and not use the user interface of Visual Studio for it. I am looking for direct access into the Dynamic Symbolic Execution part of Intellitest so that I can pass it some form of code or call and ask it what the paths are.

    I could do this by calling Z3 but then why go through all that trouble if Microsoft already figured that out for me.

    Friday, November 24, 2017 7:29 PM
  • >>Is there a class in Microsoft.Pex.Framework.dll which will solve the path conditions for me if I pass this method to it?

    I'm afraid not, according to the IntelliTest official doc. which does not mention any class that could make it.

    As Jack had suggested, you could post a thread on stack overflow where the PEX team there might give you some other advice.

    Your understanding and cooperation will be grateful.

    Have a good day:)

     

    Regards,

    Fletcher


    MSDN Community Support
    Please remember to click "Mark as Answer" the responses that resolved your issue, and to click "Unmark as Answer" if not. This can be beneficial to other community members reading this thread. If you have any compliments or complaints to MSDN Support, feel free to contact MSDNFSF@microsoft.com.



    Monday, November 27, 2017 8:18 AM