Sign in
Microsoft.com
 
Microsoft
 
 
 

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

 > 

  • Question

  • Question
    Sign in to vote
    1
    Sign in to vote

    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

  • Question
    Sign in to vote
    0
    Sign in to vote

    >>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

  • Question
    Sign in to vote
    0
    Sign in to vote
    I am trying to find the paths for variable a in the above method.
    Friday, November 10, 2017 3:12 AM
  • Question
    Sign in to vote
    0
    Sign in to vote
    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
  • Question
    Sign in to vote
    0
    Sign in to vote

    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
  • Question
    Sign in to vote
    0
    Sign in to vote

    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
  • Question
    Sign in to vote
    0
    Sign in to vote

    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
  • Question
    Sign in to vote
    0
    Sign in to vote

    >>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